![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con1d | Structured version Visualization version Unicode version |
Description: A contraposition deduction. (Contributed by NM, 27-Dec-1992.) |
Ref | Expression |
---|---|
con1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
con1d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con1d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | notnot1 127 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6 34 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con4d 109 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: mt3d 130 con1 133 pm2.24d 139 con3d 140 pm2.61d 163 pm2.8 866 dedlem0b 970 meredith 1535 hbnt 1987 axc11nlem 2032 axc11nlemALT 2153 necon3bd 2650 necon1bd 2654 sspss 3544 neldif 3570 ssonprc 6646 limsssuc 6704 limom 6734 onfununi 7086 pw2f1olem 7702 domtriord 7744 pssnn 7816 ordtypelem10 8068 rankxpsuc 8379 carden2a 8426 fidomtri2 8454 alephdom 8538 isf32lem12 8820 isfin1-3 8842 isfin7-2 8852 entric 9008 inttsk 9225 zeo 11050 zeo2 11051 xrlttri 11467 xaddf 11546 elfzonelfzo 12042 fzonfzoufzol 12043 elfznelfzo 12045 om2uzf1oi 12199 hashnfinnn0 12574 ruclem3 14334 bitsinv1lem 14464 sadcaddlem 14480 phiprmpw 14773 iserodd 14834 fldivp1 14891 prmpwdvds 14897 vdwlem6 14985 sylow2alem2 17319 efgs1b 17435 fctop 20068 cctop 20070 ppttop 20071 iccpnfcnv 22021 iccpnfhmeo 22022 iscau2 22296 ovolicc2lem2 22520 mbfeqalem 22647 limccnp2 22896 radcnv0 23420 psercnlem1 23429 pserdvlem2 23432 logtayl 23654 cxpsqrt 23697 leibpilem1 23915 rlimcnp2 23941 amgm 23965 pntpbnd1 24473 pntlem3 24496 atssma 28080 spc2d 28156 supxrnemnf 28403 xrge0iifcnv 28788 eulerpartlemf 29252 arg-ax 31125 bj-axc11nlemv 31392 pw2f1ocnv 35937 pm10.57 36764 con5 36923 con3ALT 36931 afvco2 38716 islininds2 40550 |
Copyright terms: Public domain | W3C validator |