Theorem cut1 10

Description: Modus ponens like inference.

Hypotheses

Ref	Expression
cut1.1	⊦ 𝜑
cut1.2	⊦ (~ 𝜑 ⅋ 𝜓)

Assertion

Ref	Expression
cut1	⊦ 𝜓

Proof of Theorem cut1

Step	Hyp	Ref	Expression
1		cut1.1	. . . 4 ⊦ 𝜑
2	1	ax-ibot 4	. . 3 ⊦ (⊥ ⅋ 𝜑)
3		cut1.2	. . 3 ⊦ (~ 𝜑 ⅋ 𝜓)
4	2, 3	ax-cut 6	. 2 ⊦ (⊥ ⅋ 𝜓)
5	4	ax-ebot 5	1 ⊦ 𝜓

Syntax hints:  ⊥wbot 1   ⅋ wmd 2  ~ wneg 3

This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6

This theorem is referenced by:  mdcoi  12  mdasi  14  itopi  41  lb1d  57  lb2d  58  lbi1s  87  lbi2s  88