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

Theorem syl 75
Description: Syllogism using linear implication.
Hypotheses
Ref Expression
syl.1 (𝜑𝜓)
syl.2 (𝜓𝜒)
Assertion
Ref Expression
syl (𝜑𝜒)

Proof of Theorem syl
StepHypRef Expression
1 syl.1 . . . 4 (𝜑𝜓)
2 df-li 62 . . . 4 ((𝜑𝜓) ⧟ (~ 𝜑𝜓))
31, 2lb1i 59 . . 3 (~ 𝜑𝜓)
4 syl.2 . . . 4 (𝜓𝜒)
5 df-li 62 . . . 4 ((𝜓𝜒) ⧟ (~ 𝜓𝜒))
64, 5lb1i 59 . . 3 (~ 𝜓𝜒)
73, 6ax-cut 6 . 2 (~ 𝜑𝜒)
8 df-li 62 . 2 ((𝜑𝜒) ⧟ (~ 𝜑𝜒))
97, 8lb2i 60 1 (𝜑𝜒)
Colors of variables: wff var nilad
Syntax hints:  wmd 2  ~ wneg 3  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:  dflb2s  92  licon  94  lbeui  99  md2  114  mcco  115  abs1  178
  Copyright terms: Public domain W3C validator