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 148. Its associated inference is mt3 202. (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 143 | 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 153 nsyl4 161 impi 165 simplim 168 nbior 881 pm5.55 942 pm3.13 988 rb-ax2 1745 rb-ax3 1746 rb-ax4 1747 spimfw 1959 hba1w 2045 hbe1a 2139 sp 2172 axc4 2331 exmoeu 2659 moanimlem 2696 moexexlem 2704 necon1bi 3041 fvrn0 6691 nfunsn 6700 mpoxneldm 7867 mpoxopxnop0 7870 ixpprc 8471 fineqv 8721 unbndrank 9259 pf1rcl 20440 stri 29961 hstri 29969 ddemeas 31394 hbntg 32947 bj-modalb 33947 wl-nax6im 34640 hba1-o 35913 axc5c711 35934 naecoms-o 35943 axc5c4c711 40610 hbntal 40764 |
Copyright terms: Public domain | W3C validator |