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

Theorem lb2d 58
Description: Reverse deduction using .
Hypotheses
Ref Expression
lb2d.1 (𝜑𝜒)
lb2d.2 (𝜓𝜒)
Assertion
Ref Expression
lb2d (𝜑𝜓)

Proof of Theorem lb2d
StepHypRef Expression
1 lb2d.1 . 2 (𝜑𝜒)
2 lb2d.2 . . . 4 (𝜓𝜒)
3 df-lb 56 . . . . 5 ((~ (𝜓𝜒) ⅋ ((~ 𝜓𝜒) & (~ 𝜒𝜓))) & (~ ((~ 𝜓𝜒) & (~ 𝜒𝜓)) ⅋ (𝜓𝜒)))
43eac1i 38 . . . 4 (~ (𝜓𝜒) ⅋ ((~ 𝜓𝜒) & (~ 𝜒𝜓)))
52, 4cut1 10 . . 3 ((~ 𝜓𝜒) & (~ 𝜒𝜓))
65eac2i 40 . 2 (~ 𝜒𝜓)
71, 6ax-cut 6 1 (𝜑𝜓)
Colors of variables: wff var nilad
Syntax hints:  wmd 2  ~ wneg 3   & wac 30  wlb 55
This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6  ax-init 7  ax-mdco 8  ax-eac1 33  ax-eac2 34
This theorem depends on definitions:  df-lb 56
This theorem is referenced by:  lb2i  60  dfli2  64  lb2s  68  ilbd  97
  Copyright terms: Public domain W3C validator