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 577 | . . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓)) | |
3 | 1, 2 | syl6 33 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓))) |
4 | 3 | com23 77 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓))) |
5 | pm2.01 578 | . 2 ⊢ ((𝜓 → ¬ 𝜓) → ¬ 𝜓) | |
6 | 4, 5 | syl6 33 | 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 576 ax-in2 577 |
This theorem is referenced by: mt2d 587 con3d 593 pm3.2im 598 con2 604 pm2.65 617 con1biimdc 800 exists2 2038 necon2ad 2302 necon2bd 2303 minel 3305 nlimsucg 4309 poirr2 4737 funun 4964 imadif 4999 infnlbti 6439 addnidpig 6526 zltnle 8397 zdcle 8424 btwnnz 8441 prime 8446 icc0r 8949 fznlem 9060 qltnle 9255 bcval4 9679 2sqpwodd 10554 |
Copyright terms: Public domain | W3C validator |