Theorem mdasr 15

Description: ⅋ is associative. Reverse of ax-mdas 9.

Assertion

Ref	Expression
mdasr	⊦ (~ (𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))

Proof of Theorem mdasr

Step	Hyp	Ref	Expression
1		ax-mdco 8	. . . . 5 ⊦ (~ (𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⅋ ((𝜓 ⅋ 𝜒) ⅋ 𝜑))
2		ax-mdas 9	. . . . 5 ⊦ (~ ((𝜓 ⅋ 𝜒) ⅋ 𝜑) ⅋ (𝜓 ⅋ (𝜒 ⅋ 𝜑)))
3	1, 2	ax-cut 6	. . . 4 ⊦ (~ (𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⅋ (𝜓 ⅋ (𝜒 ⅋ 𝜑)))
4		ax-mdco 8	. . . 4 ⊦ (~ (𝜓 ⅋ (𝜒 ⅋ 𝜑)) ⅋ ((𝜒 ⅋ 𝜑) ⅋ 𝜓))
5	3, 4	ax-cut 6	. . 3 ⊦ (~ (𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⅋ ((𝜒 ⅋ 𝜑) ⅋ 𝜓))
6		ax-mdas 9	. . 3 ⊦ (~ ((𝜒 ⅋ 𝜑) ⅋ 𝜓) ⅋ (𝜒 ⅋ (𝜑 ⅋ 𝜓)))
7	5, 6	ax-cut 6	. 2 ⊦ (~ (𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⅋ (𝜒 ⅋ (𝜑 ⅋ 𝜓)))
8		ax-mdco 8	. 2 ⊦ (~ (𝜒 ⅋ (𝜑 ⅋ 𝜓)) ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))
9	7, 8	ax-cut 6	1 ⊦ (~ (𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))

Syntax hints:   ⅋ wmd 2  ~ wneg 3

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

This theorem is referenced by:  mdasrd  16