Linear Logic Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > LLPE Home > Th. List > licon | Structured version |
Description: Contrapositive rule for linear implication. This follows quite neatly from df-li 62. |
Ref | Expression |
---|---|
licon | ⊦ ((𝜑 ⊸ 𝜓) ⊸ (~ 𝜓 ⊸ ~ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 77 | . . 3 ⊦ ((𝜑 ⊸ 𝜓) ⊸ (𝜑 ⊸ 𝜓)) | |
2 | df-li 62 | . . 3 ⊦ ((𝜑 ⊸ 𝜓) ⧟ (~ 𝜑 ⅋ 𝜓)) | |
3 | 1, 2 | lb1s 67 | . 2 ⊦ ((𝜑 ⊸ 𝜓) ⊸ (~ 𝜑 ⅋ 𝜓)) |
4 | dnis 78 | . . . . . . 7 ⊦ (𝜓 ⊸ ~ ~ 𝜓) | |
5 | 4 | mdm2s 74 | . . . . . 6 ⊦ ((~ 𝜑 ⅋ 𝜓) ⊸ (~ 𝜑 ⅋ ~ ~ 𝜓)) |
6 | 5 | dfli1i 65 | . . . . 5 ⊦ (~ (~ 𝜑 ⅋ 𝜓) ⅋ (~ 𝜑 ⅋ ~ ~ 𝜓)) |
7 | 6 | mdcod 11 | . . . 4 ⊦ (~ (~ 𝜑 ⅋ 𝜓) ⅋ (~ ~ 𝜓 ⅋ ~ 𝜑)) |
8 | 7 | dfli2i 66 | . . 3 ⊦ ((~ 𝜑 ⅋ 𝜓) ⊸ (~ ~ 𝜓 ⅋ ~ 𝜑)) |
9 | df-li 62 | . . 3 ⊦ ((~ 𝜓 ⊸ ~ 𝜑) ⧟ (~ ~ 𝜓 ⅋ ~ 𝜑)) | |
10 | 8, 9 | lb2s 68 | . 2 ⊦ ((~ 𝜑 ⅋ 𝜓) ⊸ (~ 𝜓 ⊸ ~ 𝜑)) |
11 | 3, 10 | syl 75 | 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-mdas 9 ax-eac1 33 ax-eac2 34 |
This theorem depends on definitions: df-lb 56 df-li 62 |
This theorem is referenced by: mcco 115 |
Copyright terms: Public domain | W3C validator |