![]() |
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 139 | . . 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: mt3d 143 con1 146 pm2.24d 149 con3d 150 pm2.61d 172 pm2.8 958 dedlem0b 1028 meredith 1685 axc16nf 2236 necon3bd 2983 necon1bd 2987 sspss 3928 neldif 3958 ssonprc 7270 limsssuc 7328 limom 7358 onfununi 7721 pw2f1olem 8352 domtriord 8394 pssnn 8466 ordtypelem10 8721 rankxpsuc 9042 carden2a 9125 fidomtri2 9153 alephdom 9237 isf32lem12 9521 isfin1-3 9543 isfin7-2 9553 entric 9714 inttsk 9931 zeo 11815 zeo2 11816 xrlttri 12282 xaddf 12367 elfzonelfzo 12889 fzonfzoufzol 12890 elfznelfzo 12892 om2uzf1oi 13071 hashnfinnn0 13467 ruclem3 15366 sumodd 15518 bitsinv1lem 15569 sadcaddlem 15585 phiprmpw 15885 iserodd 15944 fldivp1 16005 prmpwdvds 16012 vdwlem6 16094 sylow2alem2 18417 efgs1b 18533 fctop 21216 cctop 21218 ppttop 21219 iccpnfcnv 23151 iccpnfhmeo 23152 iscau2 23483 ovolicc2lem2 23722 mbfeqalem1 23845 limccnp2 24093 radcnv0 24607 psercnlem1 24616 pserdvlem2 24619 logtayl 24843 cxpsqrt 24886 leibpilem1OLD 25119 rlimcnp2 25145 amgm 25169 pntpbnd1 25727 pntlem3 25750 atssma 29809 spc2d 29885 supxrnemnf 30099 xrge0iifcnv 30577 eulerpartlemf 31030 nolesgn2o 32413 arg-ax 32998 pw2f1ocnv 38563 clsk1independent 39300 pm10.57 39526 con5 39682 con3ALT2 39690 xrred 40489 afvco2 42217 islininds2 43288 |
Copyright terms: Public domain | W3C validator |