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 523 pclem6 971 hba1w 1974 hba1wOLD 1975 axc4 2130 festino 2571 calemes 2581 fresison 2583 calemos 2584 fesapo 2585 necon3ai 2819 necon2ai 2823 necon2bi 2824 eueq3 3381 ssnpss 3710 psstr 3711 elndif 3734 n0i 3920 axnulALT 4787 nfcvb 4898 zfpair 4904 onxpdisj 5847 funtpgOLD 5943 ftpg 6423 nlimsucg 7042 reldmtpos 7360 bren2 7986 sdom0 8092 domunsn 8110 sdom1 8160 enp1i 8195 alephval3 8933 dfac2 8953 cdainflem 9013 ackbij1lem18 9059 isfin4-3 9137 fincssdom 9145 fin23lem41 9174 fin45 9214 fin17 9216 fin1a2lem7 9228 axcclem 9279 pwcfsdom 9405 canthp1lem1 9474 hargch 9495 winainflem 9515 ltxrlt 10108 xmullem2 12095 rexmul 12101 xlemul1a 12118 fzdisj 12368 lcmfunsnlem2lem2 15352 pmtrdifellem4 17899 psgnunilem3 17916 frgpcyg 19922 dvlog2lem 24398 lgsval2lem 25032 strlem1 29109 chrelat2i 29224 dfrdg4 32058 finminlem 32312 bj-nimn 32551 bj-modald 32661 finxpreclem3 33230 finxpreclem5 33232 hba1-o 34182 hlrelat2 34689 cdleme50ldil 35836 or3or 38319 stoweidlem14 40231 alneu 41201 2nodd 41812 elsetrecslem 42444 |
Copyright terms: Public domain | W3C validator |