![]() |
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 884 pm3.13 991 rb-ax2 1753 rb-ax3 1754 rb-ax4 1755 spimfw 1967 hba1w 2048 hbe1a 2138 sp 2174 axc4 2312 exmoeu 2573 necon1bi 2967 fvrn0 6922 nfunsn 6934 mpoxneldm 8201 mpoxopxnop0 8204 ixpprc 8917 fineqv 9267 unbndrank 9841 pf1rcl 22090 stri 31775 hstri 31783 ddemeas 33530 hbntg 35079 bj-modalb 35899 hba1-o 38072 axc5c711 38093 naecoms-o 38102 axc5c4c711 43464 hbntal 43618 |
Copyright terms: Public domain | W3C validator |