Axiom ax-mdas 9

Description: ⅋ is associative.

Assertion

Ref	Expression
ax-mdas	⊦ (~ ((𝜑 ⅋ 𝜓) ⅋ 𝜒) ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))

Detailed syntax breakdown of Axiom ax-mdas

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

This axiom is referenced by:  mdasd  13  mdasi  14  mdasr  15  mdas  110