![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con2i | Structured version Visualization version GIF version |
Description: A contraposition inference. Its associated inference is mt2 191. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.) |
Ref | Expression |
---|---|
con2i.a | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
con2i | ⊢ (𝜓 → ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2i.a | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | id 22 | . 2 ⊢ (𝜓 → 𝜓) | |
3 | 1, 2 | nsyl3 133 | 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: nsyl 135 notnot 136 pm2.65i 185 pm3.14 522 pclem6 991 hba1w 2016 hba1wOLD 2017 axc4 2168 festino 2600 calemes 2610 fresison 2612 calemos 2613 fesapo 2614 necon3ai 2848 necon2ai 2852 necon2bi 2853 eueq3 3414 ssnpss 3743 psstr 3744 elndif 3767 n0i 3953 axnulALT 4820 nfcvb 4928 zfpair 4934 onxpdisj 5885 funtpgOLD 5981 ftpg 6463 nlimsucg 7084 reldmtpos 7405 bren2 8028 sdom0 8133 domunsn 8151 sdom1 8201 enp1i 8236 alephval3 8971 dfac2 8991 cdainflem 9051 ackbij1lem18 9097 isfin4-3 9175 fincssdom 9183 fin23lem41 9212 fin45 9252 fin17 9254 fin1a2lem7 9266 axcclem 9317 pwcfsdom 9443 canthp1lem1 9512 hargch 9533 winainflem 9553 ltxrlt 10146 xmullem2 12133 rexmul 12139 xlemul1a 12156 fzdisj 12406 lcmfunsnlem2lem2 15399 pmtrdifellem4 17945 psgnunilem3 17962 frgpcyg 19970 dvlog2lem 24443 lgsval2lem 25077 strlem1 29237 chrelat2i 29352 dfrdg4 32183 finminlem 32437 bj-nimn 32676 bj-modald 32786 finxpreclem3 33360 finxpreclem5 33362 hba1-o 34501 hlrelat2 35007 cdleme50ldil 36153 or3or 38636 stoweidlem14 40549 alneu 41522 2nodd 42137 elsetrecslem 42770 |
Copyright terms: Public domain | W3C validator |