![]() |
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 200. (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 141 | 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 150 nsyl4 158 nsyl5 159 impi 164 simplim 167 nbior 885 pm3.13 992 rb-ax2 1747 rb-ax3 1748 rb-ax4 1749 spimfw 1961 hba1w 2042 hbe1a 2132 sp 2171 axc4 2309 exmoeu 2569 necon1bi 2958 fvrn0 6926 nfunsn 6938 mpoxneldm 8218 mpoxopxnop0 8221 ixpprc 8938 fineqv 9288 unbndrank 9867 pf1rcl 22293 stri 32139 hstri 32147 ddemeas 33983 hbntg 35529 bj-modalb 36321 hba1-o 38496 axc5c711 38517 naecoms-o 38526 nfa1w 42232 axc5c4c711 43977 hbntal 44131 |
Copyright terms: Public domain | W3C validator |