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 885 pm3.13 992 rb-ax2 1756 rb-ax3 1757 rb-ax4 1758 spimfw 1969 hba1w 2050 hbe1a 2140 sp 2176 axc4 2315 exmoeu 2581 necon1bi 2972 fvrn0 6794 nfunsn 6803 mpoxneldm 8015 mpoxopxnop0 8018 ixpprc 8694 fineqv 9025 unbndrank 9610 pf1rcl 21525 stri 30627 hstri 30635 ddemeas 32212 hbntg 33789 bj-modalb 34906 hba1-o 36919 axc5c711 36940 naecoms-o 36949 axc5c4c711 42000 hbntal 42154 |
Copyright terms: Public domain | W3C validator |