|   | 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 201. (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 887 pm3.13 996 rb-ax2 1752 rb-ax3 1753 rb-ax4 1754 spimfw 1964 hba1w 2046 hbe1a 2143 sp 2182 axc4 2320 exmoeu 2580 necon1bi 2968 fvrn0 6935 nfunsn 6947 mpoxneldm 8238 mpoxopxnop0 8241 ixpprc 8960 fineqv 9300 unbndrank 9883 pf1rcl 22354 stri 32277 hstri 32285 ddemeas 34238 hbntg 35807 bj-modalb 36718 hba1-o 38899 axc5c711 38920 naecoms-o 38929 axc5c4c711 44425 hbntal 44578 resinsnlem 48777 | 
| Copyright terms: Public domain | W3C validator |