Theorem cutf 22

Description: Left-hand version of ax-cut 6.

Hypotheses

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

Assertion

Ref	Expression
cutf	⊦ (𝜒 ⅋ 𝜑)

Proof of Theorem cutf

Step	Hyp	Ref	Expression
1		cutf.1	. . . 4 ⊦ (𝜓 ⅋ 𝜑)
2	1	mdcoi 12	. . 3 ⊦ (𝜑 ⅋ 𝜓)
3		cutf.2	. . 3 ⊦ (~ 𝜓 ⅋ 𝜒)
4	2, 3	ax-cut 6	. 2 ⊦ (𝜑 ⅋ 𝜒)
5	4	mdcoi 12	1 ⊦ (𝜒 ⅋ 𝜑)

Syntax hints:   ⅋ wmd 2  ~ wneg 3

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

This theorem is referenced by: (None)