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 589 | . . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓)) | |
3 | 1, 2 | syl6 33 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓))) |
4 | 3 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓))) |
5 | pm2.01 590 | . 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-mp 5 ax-1 6 ax-2 7 ax-in1 588 ax-in2 589 |
This theorem is referenced by: mt2d 599 con3d 605 pm3.2im 611 con2 617 pm2.65 633 con1biimdc 843 exists2 2074 necon2ad 2342 necon2bd 2343 minel 3394 nlimsucg 4451 poirr2 4901 funun 5137 imadif 5173 infnlbti 6881 mkvprop 7000 addnidpig 7112 zltnle 9068 zdcle 9095 btwnnz 9113 prime 9118 icc0r 9677 fznlem 9789 qltnle 9991 bcval4 10466 seq3coll 10553 fsum3cvg 11114 fsumsplit 11144 2sqpwodd 11781 |
Copyright terms: Public domain | W3C validator |