![]() |
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 136 | . . 3 ⊢ (𝜒 → ¬ ¬ 𝜒) | |
3 | 1, 2 | syl6 35 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒)) |
4 | 3 | con4d 114 | 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 140 con1 143 pm2.24d 147 con3d 148 pm2.61d 170 pm2.8 931 dedlem0b 1031 meredith 1703 axc16nf 2272 hbntOLD 2280 necon3bd 2934 necon1bd 2938 sspss 3836 neldif 3866 ssonprc 7145 limsssuc 7203 limom 7233 onfununi 7595 pw2f1olem 8217 domtriord 8259 pssnn 8331 ordtypelem10 8585 rankxpsuc 8906 carden2a 8953 fidomtri2 8981 alephdom 9065 isf32lem12 9349 isfin1-3 9371 isfin7-2 9381 entric 9542 inttsk 9759 zeo 11626 zeo2 11627 xrlttri 12136 xaddf 12219 elfzonelfzo 12735 fzonfzoufzol 12736 elfznelfzo 12738 om2uzf1oi 12917 hashnfinnn0 13315 ruclem3 15132 sumodd 15284 bitsinv1lem 15336 sadcaddlem 15352 phiprmpw 15654 iserodd 15713 fldivp1 15774 prmpwdvds 15781 vdwlem6 15863 sylow2alem2 18204 efgs1b 18320 fctop 20981 cctop 20983 ppttop 20984 iccpnfcnv 22915 iccpnfhmeo 22916 iscau2 23246 ovolicc2lem2 23457 mbfeqalem 23579 limccnp2 23826 radcnv0 24340 psercnlem1 24349 pserdvlem2 24352 logtayl 24576 cxpsqrt 24619 leibpilem1 24837 rlimcnp2 24863 amgm 24887 pntpbnd1 25445 pntlem3 25468 atssma 29517 spc2d 29593 supxrnemnf 29814 xrge0iifcnv 30259 eulerpartlemf 30712 nolesgn2o 32101 arg-ax 32692 pw2f1ocnv 38075 clsk1independent 38815 pm10.57 39041 con5 39199 con3ALT2 39207 xrred 40048 afvco2 41731 islininds2 42752 |
Copyright terms: Public domain | W3C validator |