Theorem mdasi 14

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

Hypothesis

Ref	Expression
mdasi.1	⊦ ((𝜑 ⅋ 𝜓) ⅋ 𝜒)

Assertion

Ref	Expression
mdasi	⊦ (𝜑 ⅋ (𝜓 ⅋ 𝜒))

Proof of Theorem mdasi

Step	Hyp	Ref	Expression
1		mdasi.1	. 2 ⊦ ((𝜑 ⅋ 𝜓) ⅋ 𝜒)
2		ax-mdas 9	. 2 ⊦ (~ ((𝜑 ⅋ 𝜓) ⅋ 𝜒) ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))
3	1, 2	cut1 10	1 ⊦ (𝜑 ⅋ (𝜓 ⅋ 𝜒))

Syntax hints:   ⅋ wmd 2

This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6  ax-mdas 9

This theorem is referenced by:  dismdac  46  extmdac  47  mdm2  69  licond  95  md1  113