Theorem cutneg 21

Description: Negated version of ax-cut 6.

Hypotheses

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

Assertion

Ref	Expression
cutneg	⊦ (𝜑 ⅋ 𝜒)

Proof of Theorem cutneg

Step	Hyp	Ref	Expression
1		cutneg.2	. . . 4 ⊦ (𝜓 ⅋ 𝜒)
2	1	mdcoi 12	. . 3 ⊦ (𝜒 ⅋ 𝜓)
3		cutneg.1	. . . 4 ⊦ (𝜑 ⅋ ~ 𝜓)
4	3	mdcoi 12	. . 3 ⊦ (~ 𝜓 ⅋ 𝜑)
5	2, 4	ax-cut 6	. 2 ⊦ (𝜒 ⅋ 𝜑)
6	5	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)