LLPE Home Linear Logic Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  LLPE Home  >  Th. List  >  mdasrd Structured version  

Theorem mdasrd 16
Description: is associative. Deduction form of mdasr 15.
Hypothesis
Ref Expression
mdasrd.1 (𝜃 ⅋ (𝜑 ⅋ (𝜓𝜒)))
Assertion
Ref Expression
mdasrd (𝜃 ⅋ ((𝜑𝜓) ⅋ 𝜒))

Proof of Theorem mdasrd
StepHypRef Expression
1 mdasrd.1 . 2 (𝜃 ⅋ (𝜑 ⅋ (𝜓𝜒)))
2 mdasr 15 . 2 (~ (𝜑 ⅋ (𝜓𝜒)) ⅋ ((𝜑𝜓) ⅋ 𝜒))
31, 2ax-cut 6 1 (𝜃 ⅋ ((𝜑𝜓) ⅋ 𝜒))
Colors of variables: wff var nilad
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
  Copyright terms: Public domain W3C validator