Theorem mdcoi 12

Description: ⅋ is commutative. Inference form of ax-mdco 8.

Hypothesis

Ref	Expression
mdcoi.1	⊦ (𝜑 ⅋ 𝜓)

Assertion

Ref	Expression
mdcoi	⊦ (𝜓 ⅋ 𝜑)

Proof of Theorem mdcoi

Step	Hyp	Ref	Expression
1		mdcoi.1	. 2 ⊦ (𝜑 ⅋ 𝜓)
2		ax-mdco 8	. 2 ⊦ (~ (𝜑 ⅋ 𝜓) ⅋ (𝜓 ⅋ 𝜑))
3	1, 2	cut1 10	1 ⊦ (𝜓 ⅋ 𝜑)

Syntax hints:   ⅋ wmd 2

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

This theorem is referenced by:  ibotr  18  ebotr  19  cutneg  21  cutf  22  dnid  23  dned  24  dni1  25  dne1  26  dnis  78  dnes  79  md1  113  abs1  178