Theorem mdasrd 16

Description: ⅋ is associative. Deduction form of mdasr 15.

Hypothesis

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

Assertion

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

Proof of Theorem mdasrd

Step	Hyp	Ref	Expression
1		mdasrd.1	. 2 ⊦ (𝜃 ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))
2		mdasr 15	. 2 ⊦ (~ (𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))
3	1, 2	ax-cut 6	1 ⊦ (𝜃 ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))

Syntax hints:   ⅋ wmd 2

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

This theorem is referenced by:  mdasri  17