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 143. Its associated inference is mt3 192. (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 142 | 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 146 nsyl4 156 impi 160 simplim 163 pm3.13 522 nbior 905 pm5.55 939 rb-ax2 1678 rb-ax3 1679 rb-ax4 1680 spimfw 1878 hba1w 1974 hba1wOLD 1975 hbe1a 2022 sp 2053 axc4 2130 exmoeu 2502 moanim 2529 moexex 2541 necon1bi 2822 fvrn0 6216 nfunsn 6225 mpt2xneldm 7338 mpt2xopxnop0 7341 ixpprc 7929 fineqv 8175 unbndrank 8705 pf1rcl 19713 stri 29116 hstri 29124 ddemeas 30299 hbntg 31711 bj-modalb 32706 hba1-o 34182 axc5c711 34203 naecoms-o 34212 axc5c4c711 38602 hbntal 38769 |
Copyright terms: Public domain | W3C validator |