![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con1i | Structured version Visualization version GIF version |
Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 193. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.) |
Ref | Expression |
---|---|
con1i.1 | ⊢ (¬ 𝜑 → 𝜓) |
Ref | Expression |
---|---|
con1i | ⊢ (¬ 𝜓 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜓) | |
2 | con1i.1 | . 2 ⊢ (¬ 𝜑 → 𝜓) | |
3 | 1, 2 | nsyl2 145 | 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: pm2.24i 148 nsyl4 158 impi 162 simplim 165 nbior 874 pm5.55 934 pm3.13 980 rb-ax2 1797 rb-ax3 1798 rb-ax4 1799 spimfw 2009 hba1w 2092 hbe1a 2138 sp 2167 axc4 2296 exmoeu 2601 exmoeuOLD 2632 moanimlem 2653 moexex 2668 necon1bi 2997 fvrn0 6476 nfunsn 6486 mpt2xneldm 7622 mpt2xopxnop0 7625 ixpprc 8217 fineqv 8465 unbndrank 9004 pf1rcl 20113 stri 29692 hstri 29700 ddemeas 30901 hbntg 32303 bj-modalb 33298 wl-nax6im 33899 hba1-o 35056 axc5c711 35077 naecoms-o 35086 axc5c4c711 39567 hbntal 39723 |
Copyright terms: Public domain | W3C validator |