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 142. Its associated inference is mt3 191. (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 145 nsyl4 155 impi 159 simplim 162 pm3.13 521 nbior 901 pm5.55 937 rb-ax2 1669 rb-ax3 1670 rb-ax4 1671 spimfw 1865 hba1w 1961 hba1wOLD 1962 hbe1a 2009 sp 2041 axc4 2115 exmoeu 2490 moanim 2517 moexex 2529 necon1bi 2810 fvrn0 6126 nfunsn 6135 mpt2xneldm 7225 mpt2xopxnop0 7228 ixpprc 7815 fineqv 8060 unbndrank 8588 pf1rcl 19534 wlkntrllem3 26091 stri 28500 hstri 28508 ddemeas 29626 hbntg 30955 bj-modalb 31893 wl-nf-nf2 32463 hba1-o 33200 axc5c711 33221 naecoms-o 33230 axc5c4c711 37624 hbntal 37790 |
Copyright terms: Public domain | W3C validator |