![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con1i | Structured version Visualization version Unicode version |
Description: A contraposition inference. Inference associated with con1 133. Its associated inference is mt3 185. (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 132 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 138 nsyl4 149 impi 153 simplim 156 pm3.13 508 nbior 876 pm5.55 913 rb-ax2 1647 rb-ax3 1648 rb-ax4 1649 spimfw 1806 hba1w 1894 sp 1948 axc4 1949 exmoeu 2342 moanim 2369 moexex 2381 necon1bi 2664 fvrn0 5910 nfunsn 5919 mpt2xneldm 6985 mpt2xopxnop0 6988 ixpprc 7569 fineqv 7813 unbndrank 8339 pf1rcl 18986 wlkntrllem3 25340 stri 27959 hstri 27967 ddemeas 29108 hbntg 30501 bj-naecomsv 31395 hba1-o 32514 axc5c711 32534 naecoms-o 32543 axc5c4c711 36796 hbntal 36964 |
Copyright terms: Public domain | W3C validator |