![]() |
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 7272 limsssuc 7330 limom 7360 onfununi 7723 pw2f1olem 8354 domtriord 8396 pssnn 8468 ordtypelem10 8723 rankxpsuc 9044 carden2a 9127 fidomtri2 9155 alephdom 9239 isf32lem12 9523 isfin1-3 9545 isfin7-2 9555 entric 9716 inttsk 9933 zeo 11820 zeo2 11821 xrlttri 12287 xaddf 12372 elfzonelfzo 12894 fzonfzoufzol 12895 elfznelfzo 12897 om2uzf1oi 13076 hashnfinnn0 13473 ruclem3 15375 sumodd 15528 bitsinv1lem 15579 sadcaddlem 15595 phiprmpw 15896 iserodd 15955 fldivp1 16016 prmpwdvds 16023 vdwlem6 16105 sylow2alem2 18428 efgs1b 18544 fctop 21227 cctop 21229 ppttop 21230 iccpnfcnv 23162 iccpnfhmeo 23163 iscau2 23494 ovolicc2lem2 23733 mbfeqalem1 23856 limccnp2 24104 radcnv0 24618 psercnlem1 24627 pserdvlem2 24630 logtayl 24854 cxpsqrt 24897 leibpilem1OLD 25130 rlimcnp2 25156 amgm 25180 pntpbnd1 25744 pntlem3 25767 atssma 29826 spc2d 29902 supxrnemnf 30113 xrge0iifcnv 30585 eulerpartlemf 31038 nolesgn2o 32421 arg-ax 33006 pw2f1ocnv 38577 clsk1independent 39314 pm10.57 39540 con5 39696 con3ALT2 39704 xrred 40503 afvco2 42231 islininds2 43302 |
Copyright terms: Public domain | W3C validator |