![]() |
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 615 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6 33 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | com23 78 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | pm2.01 616 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | syl6 33 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 614 ax-in2 615 |
This theorem is referenced by: mt2d 625 con3d 631 pm3.2im 637 con2 643 pm2.65 659 con1biimdc 873 exists2 2123 necon2ad 2404 necon2bd 2405 minel 3484 nlimsucg 4561 poirr2 5016 funun 5255 imadif 5291 infnlbti 7018 mkvprop 7149 addnidpig 7313 zltnle 9275 zdcle 9305 btwnnz 9323 prime 9328 icc0r 9900 fznlem 10014 qltnle 10219 bcval4 10703 seq3coll 10793 fsum3cvg 11357 fsumsplit 11386 fproddccvg 11551 fprodsplitdc 11575 2sqpwodd 12146 pockthg 12325 prmunb 12330 logbgcd1irr 14018 lgsne0 14072 |
Copyright terms: Public domain | W3C validator |