Theorem mdcod 11

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

Hypothesis

Ref	Expression
mdcod.1	⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜓))

Assertion

Ref	Expression
mdcod	⊦ (𝜃 ⅋ (𝜓 ⅋ 𝜑))

Proof of Theorem mdcod

Step	Hyp	Ref	Expression
1		mdcod.1	. 2 ⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜓))
2		ax-mdco 8	. 2 ⊦ (~ (𝜑 ⅋ 𝜓) ⅋ (𝜓 ⅋ 𝜑))
3	1, 2	ax-cut 6	1 ⊦ (𝜃 ⅋ (𝜓 ⅋ 𝜑))

Syntax hints:   ⅋ wmd 2

This theorem was proved from axioms:  ax-cut 6  ax-mdco 8

This theorem is referenced by:  mdm1  70  licon  94  licond  95  mdco  108  md1  113