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

Theorem mcco 115
Description: is commutative. TODO extract double negation theorems, licon 94 alternate forms
Assertion
Ref Expression
mcco ((𝜑𝜓) ⊸ (𝜓𝜑))

Proof of Theorem mcco
StepHypRef Expression
1 dnis 78 . . 3 ((𝜑𝜓) ⊸ ~ ~ (𝜑𝜓))
2 ax-mdco 8 . . . . . 6 (~ (~ 𝜓 ⅋ ~ 𝜑) ⅋ (~ 𝜑 ⅋ ~ 𝜓))
32dfli2i 66 . . . . 5 ((~ 𝜓 ⅋ ~ 𝜑) ⊸ (~ 𝜑 ⅋ ~ 𝜓))
4 dnis 78 . . . . . 6 ((~ 𝜑 ⅋ ~ 𝜓) ⊸ ~ ~ (~ 𝜑 ⅋ ~ 𝜓))
5 id 77 . . . . . . . 8 ((𝜑𝜓) ⊸ (𝜑𝜓))
6 df-mc 106 . . . . . . . 8 ((𝜑𝜓) ⧟ ~ (~ 𝜑 ⅋ ~ 𝜓))
75, 6lb1s 67 . . . . . . 7 ((𝜑𝜓) ⊸ ~ (~ 𝜑 ⅋ ~ 𝜓))
8 licon 94 . . . . . . 7 (((𝜑𝜓) ⊸ ~ (~ 𝜑 ⅋ ~ 𝜓)) ⊸ (~ ~ (~ 𝜑 ⅋ ~ 𝜓) ⊸ ~ (𝜑𝜓)))
97, 8lmp 76 . . . . . 6 (~ ~ (~ 𝜑 ⅋ ~ 𝜓) ⊸ ~ (𝜑𝜓))
104, 9syl 75 . . . . 5 ((~ 𝜑 ⅋ ~ 𝜓) ⊸ ~ (𝜑𝜓))
113, 10syl 75 . . . 4 ((~ 𝜓 ⅋ ~ 𝜑) ⊸ ~ (𝜑𝜓))
12 licon 94 . . . 4 (((~ 𝜓 ⅋ ~ 𝜑) ⊸ ~ (𝜑𝜓)) ⊸ (~ ~ (𝜑𝜓) ⊸ ~ (~ 𝜓 ⅋ ~ 𝜑)))
1311, 12lmp 76 . . 3 (~ ~ (𝜑𝜓) ⊸ ~ (~ 𝜓 ⅋ ~ 𝜑))
141, 13syl 75 . 2 ((𝜑𝜓) ⊸ ~ (~ 𝜓 ⅋ ~ 𝜑))
15 df-mc 106 . 2 ((𝜓𝜑) ⧟ ~ (~ 𝜓 ⅋ ~ 𝜑))
1614, 15lb2s 68 1 ((𝜑𝜓) ⊸ (𝜓𝜑))
Colors of variables: wff var nilad
Syntax hints:  wmd 2  ~ wneg 3  wli 61  wmc 105
This theorem was proved from axioms:  ax-ibot 4  ax-ebot 5  ax-cut 6  ax-init 7  ax-mdco 8  ax-mdas 9  ax-eac1 33  ax-eac2 34
This theorem depends on definitions:  df-lb 56  df-li 62  df-mc 106
This theorem is referenced by:  mccob  116
  Copyright terms: Public domain W3C validator