![]() |
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 192. (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 136 | 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 138 notnot 139 pm2.65i 186 pm3.14 1023 pclem6 1054 hba1w 2149 axc4 2352 festinoALT 2760 calemesOLD 2777 fresisonOLD 2781 calemosOLD 2783 fesapoOLD 2785 necon3ai 3024 necon2ai 3028 necon2bi 3029 eueq3 3606 ssnpss 3938 psstr 3939 elndif 3963 n0i 4151 axnulALT 5013 nfcvb 5078 zfpair 5127 onxpdisj 6086 ftpg 6679 nlimsucg 7308 reldmtpos 7630 bren2 8259 sdom0 8367 domunsn 8385 sdom1 8435 enp1i 8470 alephval3 9253 dfac2OLD 9275 cdainflem 9335 ackbij1lem18 9381 isfin4-3 9459 fincssdom 9467 fin23lem41 9496 fin45 9536 fin17 9538 fin1a2lem7 9550 axcclem 9601 pwcfsdom 9727 canthp1lem1 9796 hargch 9817 winainflem 9837 ltxrlt 10434 xmullem2 12390 rexmul 12396 xlemul1a 12413 fzdisj 12668 lcmfunsnlem2lem2 15732 pmtrdifellem4 18256 psgnunilem3 18274 frgpcyg 20288 dvlog2lem 24804 lgsval2lem 25452 strlem1 29660 chrelat2i 29775 dfrdg4 32592 finminlem 32846 bj-nimn 33074 bj-modald 33195 finxpreclem3 33774 finxpreclem5 33776 hba1-o 34971 hlrelat2 35477 cdleme50ldil 36622 or3or 39158 stoweidlem14 41023 alneu 42024 2nodd 42677 elsetrecslem 43354 |
Copyright terms: Public domain | W3C validator |