![]() |
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 143. Its associated inference is mt3 192. (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 142 | 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 146 nsyl4 156 impi 160 simplim 163 pm3.13 523 nbior 941 pm5.55 975 rb-ax2 1819 rb-ax3 1820 rb-ax4 1821 spimfw 2036 hba1w 2117 hba1wOLD 2118 hbe1a 2163 sp 2192 axc4 2269 exmoeu 2632 moanim 2659 moexex 2671 necon1bi 2952 fvrn0 6369 nfunsn 6378 mpt2xneldm 7499 mpt2xopxnop0 7502 ixpprc 8087 fineqv 8332 unbndrank 8870 pf1rcl 19907 stri 29417 hstri 29425 ddemeas 30600 hbntg 32008 bj-modalb 33004 hba1-o 34678 axc5c711 34699 naecoms-o 34708 axc5c4c711 39096 hbntal 39263 |
Copyright terms: Public domain | W3C validator |