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 610 | . . . 4 ⊢ (¬ 𝜒 → (𝜒 → ¬ 𝜓)) | |
3 | 1, 2 | syl6 33 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓))) |
4 | 3 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓))) |
5 | pm2.01 611 | . 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 609 ax-in2 610 |
This theorem is referenced by: mt2d 620 con3d 626 pm3.2im 632 con2 638 pm2.65 654 con1biimdc 868 exists2 2116 necon2ad 2397 necon2bd 2398 minel 3476 nlimsucg 4550 poirr2 5003 funun 5242 imadif 5278 infnlbti 7003 mkvprop 7134 addnidpig 7298 zltnle 9258 zdcle 9288 btwnnz 9306 prime 9311 icc0r 9883 fznlem 9997 qltnle 10202 bcval4 10686 seq3coll 10777 fsum3cvg 11341 fsumsplit 11370 fproddccvg 11535 fprodsplitdc 11559 2sqpwodd 12130 pockthg 12309 prmunb 12314 logbgcd1irr 13679 lgsne0 13733 |
Copyright terms: Public domain | W3C validator |