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 201. (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 140 | 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 142 notnot 144 pm2.65i 195 pm3.14 989 pclem6 1019 hba1w 2045 axc4 2331 festinoALT 2755 necon3ai 3038 necon2ai 3042 necon2bi 3043 eueq3 3699 ssnpss 4077 psstr 4078 elndif 4102 n0i 4296 axnulALT 5199 nfcvb 5268 zfpair 5312 epelg 5459 onxpdisj 6303 ftpg 6910 nlimsucg 7546 reldmtpos 7889 bren2 8528 sdom0 8637 domunsn 8655 sdom1 8706 enp1i 8741 alephval3 9524 cdainflem 9601 ackbij1lem18 9647 isfin4p1 9725 fincssdom 9733 fin23lem41 9762 fin17 9804 fin1a2lem7 9816 axcclem 9867 pwcfsdom 9993 canthp1lem1 10062 hargch 10083 winainflem 10103 ltxrlt 10699 xmullem2 12646 rexmul 12652 xlemul1a 12669 fzdisj 12922 lcmfunsnlem2lem2 15971 pmtrdifellem4 18536 psgnunilem3 18553 frgpcyg 20648 dvlog2lem 25162 lgsval2lem 25810 strlem1 29954 chrelat2i 30069 dfrdg4 33309 finminlem 33563 bj-nimn 33796 bj-modald 33903 finxpreclem3 34556 finxpreclem5 34558 hba1-o 35913 hlrelat2 36419 cdleme50ldil 37564 sn-dtru 38989 or3or 40249 stoweidlem14 42176 alneu 43200 2nodd 43956 smndex1n0mnd 44012 elsetrecslem 44729 |
Copyright terms: Public domain | W3C validator |