Axiom ax-mdco 8

Description: ⅋ is commutative.

Assertion

Ref	Expression
ax-mdco	⊦ (~ (𝜑 ⅋ 𝜓) ⅋ (𝜓 ⅋ 𝜑))

Detailed syntax breakdown of Axiom ax-mdco

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		wps	. . . 4 wff 𝜓
3	1, 2	wmd 2	. . 3 wff (𝜑 ⅋ 𝜓)
4	3	wneg 3	. 2 wff ~ (𝜑 ⅋ 𝜓)
5	2, 1	wmd 2	. 2 wff (𝜓 ⅋ 𝜑)
6	4, 5	wmd 2	1 wff (~ (𝜑 ⅋ 𝜓) ⅋ (𝜓 ⅋ 𝜑))

This axiom is referenced by:  mdcod  11  mdcoi  12  mdasr  15  mcco  115