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

Theorem nems 86
Description: "Why not" is monotone.
Hypothesis
Ref Expression
nems.1 (𝜑𝜓)
Assertion
Ref Expression
nems (? 𝜑 ⊸ ? 𝜓)

Proof of Theorem nems
StepHypRef Expression
1 nems.1 . . . . 5 (𝜑𝜓)
21dfli1i 65 . . . 4 (~ 𝜑𝜓)
3 ax-init 7 . . . . 5 (~ ? 𝜓 ⅋ ? 𝜓)
43ax-epe 50 . . . 4 (~ 𝜓 ⅋ ? 𝜓)
52, 4ax-cut 6 . . 3 (~ 𝜑 ⅋ ? 𝜓)
65ax-ipe 49 . 2 (~ ? 𝜑 ⅋ ? 𝜓)
76dfli2i 66 1 (? 𝜑 ⊸ ? 𝜓)
Colors of variables: wff var nilad
Syntax hints:  ~ wneg 3  ? wne 48  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  ax-ipe 49  ax-epe 50
This theorem depends on definitions:  df-lb 56  df-li 62
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator