![]() |
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 199. (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 138 | 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 140 notnot 142 pm2.65i 193 pm3.14 993 pclem6 1023 hba1w 2049 axc4 2313 festinoALT 2669 necon3aiOLD 2965 necon2ai 2969 necon2bi 2970 eueq3 3707 ssnpss 4103 psstr 4104 elndif 4128 n0i 4333 axnulALT 5304 nfcvb 5374 zfpair 5419 epelg 5581 onxpdisj 6490 ftpg 7156 nlimsucg 7835 reldmtpos 8225 bren2 8985 sdom0OLD 9115 domunsn 9133 sdom1OLD 9249 1sdom2dom 9253 enp1iOLD 9286 alephval3 10111 cdainflem 10188 ackbij1lem18 10238 isfin4p1 10316 fincssdom 10324 fin23lem41 10353 fin17 10395 fin1a2lem7 10407 axcclem 10458 pwcfsdom 10584 canthp1lem1 10653 hargch 10674 winainflem 10694 ltxrlt 11291 xmullem2 13251 rexmul 13257 xlemul1a 13274 fzdisj 13535 lcmfunsnlem2lem2 16583 smndex1n0mnd 18835 pmtrdifellem4 19395 psgnunilem3 19412 frgpcyg 21439 dvlog2lem 26500 lgsval2lem 27153 elons2 28064 strlem1 31936 chrelat2i 32051 dfrdg4 35393 finminlem 35667 bj-nimn 35904 bj-modald 36014 finxpreclem3 36738 finxpreclem5 36740 hba1-o 38231 hlrelat2 38738 cdleme50ldil 39883 lcmineqlem23 41383 onov0suclim 42487 or3or 43237 stoweidlem14 45189 alneu 46291 2nodd 47009 elsetrecslem 47906 |
Copyright terms: Public domain | W3C validator |