Theorem mdasd 13

Description: ⅋ is associative. Deduction form of ax-mdas 9.

Hypothesis

Ref	Expression
mdasd.1	⊦ (𝜃 ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))

Assertion

Ref	Expression
mdasd	⊦ (𝜃 ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))

Proof of Theorem mdasd

Step	Hyp	Ref	Expression
1		mdasd.1	. 2 ⊦ (𝜃 ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))
2		ax-mdas 9	. 2 ⊦ (~ ((𝜑 ⅋ 𝜓) ⅋ 𝜒) ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))
3	1, 2	ax-cut 6	1 ⊦ (𝜃 ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))

Syntax hints:   ⅋ wmd 2

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

This theorem is referenced by: (None)