Theorem mdasri 17

Description: ⅋ is associative. Inference form of mdasrd 16.

Hypothesis

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

Assertion

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

Proof of Theorem mdasri

Step	Hyp	Ref	Expression
1		mdasri.1	. . . 4 ⊦ (𝜑 ⅋ (𝜓 ⅋ 𝜒))
2	1	ax-ibot 4	. . 3 ⊦ (⊥ ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))
3	2	mdasrd 16	. 2 ⊦ (⊥ ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))
4	3	ax-ebot 5	1 ⊦ ((𝜑 ⅋ 𝜓) ⅋ 𝜒)

Syntax hints:  ⊥wbot 1   ⅋ wmd 2

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

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