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 190. (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 132 | 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 134 notnot 135 pm2.65i 184 pm3.14 522 pclem6 967 hba1w 1961 hba1wOLD 1962 axc4 2115 festino 2559 calemes 2569 fresison 2571 calemos 2572 fesapo 2573 necon3ai 2807 necon2ai 2811 necon2bi 2812 eueq3 3348 ssnpss 3672 psstr 3673 elndif 3696 n0i 3879 axnulALT 4715 nfcvb 4824 zfpair 4831 onxpdisj 5764 funtpgOLD 5857 ftpg 6328 nlimsucg 6934 reldmtpos 7247 bren2 7872 sdom0 7977 domunsn 7995 sdom1 8045 enp1i 8080 alephval3 8816 dfac2 8836 cdainflem 8896 ackbij1lem18 8942 isfin4-3 9020 fincssdom 9028 fin23lem41 9057 fin45 9097 fin17 9099 fin1a2lem7 9111 axcclem 9162 pwcfsdom 9284 canthp1lem1 9353 hargch 9374 winainflem 9394 ltxrlt 9987 xmullem2 11967 rexmul 11973 xlemul1a 11990 fzdisj 12239 lcmfunsnlem2lem2 15190 pmtrdifellem4 17722 psgnunilem3 17739 frgpcyg 19741 dvlog2lem 24198 lgsval2lem 24832 isusgra0 25876 usgraop 25879 cusgrares 26001 2pthlem2 26126 2spot0 26591 strlem1 28493 chrelat2i 28608 dfrdg4 31228 finminlem 31482 bj-nimn 31721 bj-modald 31848 finxpreclem3 32406 finxpreclem5 32408 hba1-o 33200 hlrelat2 33707 cdleme50ldil 34854 or3or 37339 stoweidlem14 38907 alneu 39850 2nodd 41602 elsetrecslem 42243 |
Copyright terms: Public domain | W3C validator |