![]() |
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 142 | . . 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: con1 146 mt3d 148 pm2.24d 151 con3d 152 pm2.61d 179 pm2.8 970 dedlem0b 1042 meredith 1635 necon3bd 2943 necon1bd 2947 spc2d 3586 sspss 4095 neldif 4126 ssonprc 7791 limsssuc 7855 limom 7887 onfununi 8362 pw2f1olem 9101 domtriord 9148 pssnn 9193 pssnnOLD 9290 ordtypelem10 9552 rankxpsuc 9907 carden2a 9991 fidomtri2 10019 alephdom 10106 isf32lem12 10389 isfin1-3 10411 isfin7-2 10421 entric 10582 inttsk 10799 zeo 12681 zeo2 12682 xrlttri 13153 xaddf 13238 elfzonelfzo 13770 fzonfzoufzol 13771 elfznelfzo 13773 om2uzf1oi 13954 hashnfinnn0 14356 ruclem3 16213 sumodd 16368 bitsinv1lem 16419 sadcaddlem 16435 phiprmpw 16748 iserodd 16807 fldivp1 16869 prmpwdvds 16876 vdwlem6 16958 sylow2alem2 19585 efgs1b 19703 fctop 22951 cctop 22953 ppttop 22954 iccpnfcnv 24913 iccpnfhmeo 24914 iscau2 25249 ovolicc2lem2 25491 mbfeqalem1 25614 limccnp2 25865 radcnv0 26397 psercnlem1 26407 pserdvlem2 26410 logtayl 26639 cxpsqrt 26682 rlimcnp2 26943 amgm 26968 pntpbnd1 27564 pntlem3 27587 nolesgn2o 27650 nogesgn1o 27652 atssma 32260 fsuppcurry1 32589 fsuppcurry2 32590 supxrnemnf 32620 xrge0iifcnv 33665 eulerpartlemf 34121 cusgracyclt3v 34897 arg-ax 36031 pw2f1ocnv 42600 onsupnmax 42798 infordmin 43104 clsk1independent 43618 pm10.57 43950 con5 44103 con3ALT2 44111 xrred 44885 afvco2 46694 islininds2 47738 |
Copyright terms: Public domain | W3C validator |