![]() |
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 138 | . . 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 142 con1 145 pm2.24d 148 con3d 149 pm2.61d 171 pm2.8 947 dedlem0b 1029 meredith 1714 axc16nf 2302 hbntOLD 2310 necon3bd 2957 necon1bd 2961 sspss 3857 neldif 3887 ssonprc 7140 limsssuc 7198 limom 7228 onfununi 7592 pw2f1olem 8221 domtriord 8263 pssnn 8335 ordtypelem10 8589 rankxpsuc 8910 carden2a 8993 fidomtri2 9021 alephdom 9105 isf32lem12 9389 isfin1-3 9411 isfin7-2 9421 entric 9582 inttsk 9799 zeo 11666 zeo2 11667 xrlttri 12178 xaddf 12261 elfzonelfzo 12779 fzonfzoufzol 12780 elfznelfzo 12782 om2uzf1oi 12961 hashnfinnn0 13355 ruclem3 15169 sumodd 15320 bitsinv1lem 15372 sadcaddlem 15388 phiprmpw 15689 iserodd 15748 fldivp1 15809 prmpwdvds 15816 vdwlem6 15898 sylow2alem2 18241 efgs1b 18357 fctop 21030 cctop 21032 ppttop 21033 iccpnfcnv 22964 iccpnfhmeo 22965 iscau2 23295 ovolicc2lem2 23507 mbfeqalem 23630 limccnp2 23877 radcnv0 24391 psercnlem1 24400 pserdvlem2 24403 logtayl 24628 cxpsqrt 24671 leibpilem1 24889 rlimcnp2 24915 amgm 24939 pntpbnd1 25497 pntlem3 25520 atssma 29578 spc2d 29654 supxrnemnf 29875 xrge0iifcnv 30320 eulerpartlemf 30773 nolesgn2o 32162 arg-ax 32753 pw2f1ocnv 38131 clsk1independent 38871 pm10.57 39097 con5 39254 con3ALT2 39262 xrred 40098 afvco2 41777 islininds2 42802 |
Copyright terms: Public domain | W3C validator |