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

Theorem lbi2s 88
Description: Extract reverse implication from biconditional. Syllogism form of lb2i 60.
Assertion
Ref Expression
lbi2s ((𝜑𝜓) ⊸ (𝜓𝜑))

Proof of Theorem lbi2s
StepHypRef Expression
1 df-lb 56 . . . . 5 ((~ (𝜑𝜓) ⅋ ((~ 𝜑𝜓) & (~ 𝜓𝜑))) & (~ ((~ 𝜑𝜓) & (~ 𝜓𝜑)) ⅋ (𝜑𝜓)))
21eac1i 38 . . . 4 (~ (𝜑𝜓) ⅋ ((~ 𝜑𝜓) & (~ 𝜓𝜑)))
32ax-eac2 34 . . 3 (~ (𝜑𝜓) ⅋ (~ 𝜓𝜑))
4 df-li 62 . . . 4 ((𝜓𝜑) ⧟ (~ 𝜓𝜑))
5 df-lb 56 . . . . . 6 ((~ ((𝜓𝜑) ⧟ (~ 𝜓𝜑)) ⅋ ((~ (𝜓𝜑) ⅋ (~ 𝜓𝜑)) & (~ (~ 𝜓𝜑) ⅋ (𝜓𝜑)))) & (~ ((~ (𝜓𝜑) ⅋ (~ 𝜓𝜑)) & (~ (~ 𝜓𝜑) ⅋ (𝜓𝜑))) ⅋ ((𝜓𝜑) ⧟ (~ 𝜓𝜑))))
65eac1i 38 . . . . 5 (~ ((𝜓𝜑) ⧟ (~ 𝜓𝜑)) ⅋ ((~ (𝜓𝜑) ⅋ (~ 𝜓𝜑)) & (~ (~ 𝜓𝜑) ⅋ (𝜓𝜑))))
76ax-eac2 34 . . . 4 (~ ((𝜓𝜑) ⧟ (~ 𝜓𝜑)) ⅋ (~ (~ 𝜓𝜑) ⅋ (𝜓𝜑)))
84, 7cut1 10 . . 3 (~ (~ 𝜓𝜑) ⅋ (𝜓𝜑))
93, 8ax-cut 6 . 2 (~ (𝜑𝜓) ⅋ (𝜓𝜑))
10 df-li 62 . 2 (((𝜑𝜓) ⊸ (𝜓𝜑)) ⧟ (~ (𝜑𝜓) ⅋ (𝜓𝜑)))
119, 10lb2i 60 1 ((𝜑𝜓) ⊸ (𝜓𝜑))
Colors of variables: wff var nilad
Syntax hints:  wmd 2  ~ wneg 3   & wac 30  wlb 55  wli 61
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  df-li 62
This theorem is referenced by:  lbi2  90  dflb1s  91
  Copyright terms: Public domain W3C validator