Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > con2d | Unicode 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 605 | . . . 4 | |
3 | 1, 2 | syl6 33 | . . 3 |
4 | 3 | com23 78 | . 2 |
5 | pm2.01 606 | . 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 604 ax-in2 605 |
This theorem is referenced by: mt2d 615 con3d 621 pm3.2im 627 con2 633 pm2.65 649 con1biimdc 863 exists2 2110 necon2ad 2391 necon2bd 2392 minel 3465 nlimsucg 4537 poirr2 4990 funun 5226 imadif 5262 infnlbti 6982 mkvprop 7113 addnidpig 7268 zltnle 9228 zdcle 9258 btwnnz 9276 prime 9281 icc0r 9853 fznlem 9966 qltnle 10171 bcval4 10654 seq3coll 10741 fsum3cvg 11305 fsumsplit 11334 fproddccvg 11499 fprodsplitdc 11523 2sqpwodd 12087 pockthg 12266 logbgcd1irr 13432 |
Copyright terms: Public domain | W3C validator |