![]() |
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 578 | . . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓)) | |
3 | 1, 2 | syl6 33 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓))) |
4 | 3 | com23 77 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓))) |
5 | pm2.01 579 | . 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 577 ax-in2 578 |
This theorem is referenced by: mt2d 588 con3d 594 pm3.2im 599 con2 605 pm2.65 618 con1biimdc 801 exists2 2039 necon2ad 2303 necon2bd 2304 minel 3312 nlimsucg 4317 poirr2 4747 funun 4974 imadif 5010 infnlbti 6498 addnidpig 6588 zltnle 8478 zdcle 8505 btwnnz 8522 prime 8527 icc0r 9025 fznlem 9136 qltnle 9332 bcval4 9776 fisumcvg 10338 2sqpwodd 10698 |
Copyright terms: Public domain | W3C validator |