Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > con1d | Structured version Visualization version GIF 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 | notnot 144 | . . 3 ⊢ (𝜒 → ¬ ¬ 𝜒) | |
3 | 1, 2 | syl6 35 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒)) |
4 | 3 | con4d 115 | 1 ⊢ (𝜑 → (¬ 𝜒 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: con1 148 mt3d 150 pm2.24d 154 con3d 155 pm2.61d 180 pm2.8 966 dedlem0b 1036 meredith 1633 necon3bd 3027 necon1bd 3031 spc2d 3600 sspss 4073 neldif 4103 ssonprc 7496 limsssuc 7554 limom 7584 onfununi 7967 pw2f1olem 8609 domtriord 8651 pssnn 8724 ordtypelem10 8979 rankxpsuc 9299 carden2a 9383 fidomtri2 9411 alephdom 9495 isf32lem12 9774 isfin1-3 9796 isfin7-2 9806 entric 9967 inttsk 10184 zeo 12056 zeo2 12057 xrlttri 12520 xaddf 12605 elfzonelfzo 13127 fzonfzoufzol 13128 elfznelfzo 13130 om2uzf1oi 13309 hashnfinnn0 13710 ruclem3 15574 sumodd 15727 bitsinv1lem 15778 sadcaddlem 15794 phiprmpw 16101 iserodd 16160 fldivp1 16221 prmpwdvds 16228 vdwlem6 16310 sylow2alem2 18672 efgs1b 18791 fctop 21540 cctop 21542 ppttop 21543 iccpnfcnv 23475 iccpnfhmeo 23476 iscau2 23807 ovolicc2lem2 24046 mbfeqalem1 24169 limccnp2 24417 radcnv0 24931 psercnlem1 24940 pserdvlem2 24943 logtayl 25170 cxpsqrt 25213 rlimcnp2 25471 amgm 25495 pntpbnd1 26089 pntlem3 26112 atssma 30082 fsuppcurry1 30387 fsuppcurry2 30388 supxrnemnf 30419 xrge0iifcnv 31075 eulerpartlemf 31527 cusgracyclt3v 32300 nolesgn2o 33075 arg-ax 33661 pw2f1ocnv 39512 infordmin 39777 clsk1independent 40274 pm10.57 40580 con5 40733 con3ALT2 40741 xrred 41509 afvco2 43252 islininds2 44467 |
Copyright terms: Public domain | W3C validator |