Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > con2d | GIF version |
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.) |
Ref | Expression |
---|---|
con2d.1 | ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) |
Ref | Expression |
---|---|
con2d | ⊢ (𝜑 → (𝜒 → ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2d.1 | . . . 4 ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) | |
2 | ax-in2 545 | . . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓)) | |
3 | 1, 2 | syl6 29 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓))) |
4 | 3 | com23 72 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓))) |
5 | pm2.01 546 | . 2 ⊢ ((𝜓 → ¬ 𝜓) → ¬ 𝜓) | |
6 | 4, 5 | syl6 29 | 1 ⊢ (𝜑 → (𝜒 → ¬ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 544 ax-in2 545 |
This theorem is referenced by: mt2d 555 con3d 561 pm3.2im 566 con2 572 pm2.65 585 con1biimdc 767 exists2 1997 necon2ad 2262 necon2bd 2263 minel 3283 nlimsucg 4290 poirr2 4717 funun 4944 imadif 4979 addnidpig 6434 zltnle 8291 zdcle 8317 btwnnz 8334 prime 8337 icc0r 8795 fznlem 8905 qltnle 9101 |
Copyright terms: Public domain | W3C validator |