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 135 | . . 3 ⊢ (𝜒 → ¬ ¬ 𝜒) | |
3 | 1, 2 | syl6 34 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒)) |
4 | 3 | con4d 113 | 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 139 con1 142 pm2.24d 146 con3d 147 pm2.61d 169 pm2.8 891 dedlem0b 992 meredith 1557 axc11nlemOLD2 1975 axc16nf 2122 hbntOLD 2130 axc11nlemOLD 2146 axc11nlemALT 2294 necon3bd 2796 necon1bd 2800 sspss 3668 neldif 3697 ssonprc 6884 limsssuc 6942 limom 6972 onfununi 7325 pw2f1olem 7949 domtriord 7991 pssnn 8063 ordtypelem10 8315 rankxpsuc 8628 carden2a 8675 fidomtri2 8703 alephdom 8787 isf32lem12 9069 isfin1-3 9091 isfin7-2 9101 entric 9258 inttsk 9475 zeo 11339 zeo2 11340 xrlttri 11848 xaddf 11929 elfzonelfzo 12436 fzonfzoufzol 12437 elfznelfzo 12439 om2uzf1oi 12614 hashnfinnn0 13013 ruclem3 14801 sumodd 14949 bitsinv1lem 15001 sadcaddlem 15017 phiprmpw 15319 iserodd 15378 fldivp1 15439 prmpwdvds 15446 vdwlem6 15528 sylow2alem2 17856 efgs1b 17972 fctop 20618 cctop 20620 ppttop 20621 iccpnfcnv 22551 iccpnfhmeo 22552 iscau2 22883 ovolicc2lem2 23093 mbfeqalem 23215 limccnp2 23462 radcnv0 23974 psercnlem1 23983 pserdvlem2 23986 logtayl 24206 cxpsqrt 24249 leibpilem1 24467 rlimcnp2 24493 amgm 24517 pntpbnd1 25075 pntlem3 25098 atssma 28621 spc2d 28697 supxrnemnf 28924 xrge0iifcnv 29307 eulerpartlemf 29759 arg-ax 31585 pw2f1ocnv 36622 clsk1independent 37364 pm10.57 37592 con5 37749 con3ALT2 37757 xrred 38522 afvco2 39905 islininds2 42067 |
Copyright terms: Public domain | W3C validator |