![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3ai | Structured version Visualization version Unicode version |
Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
necon3ai.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
necon3ai |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3ai.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nne 2628 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylibr 217 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2i 125 |
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 depends on definitions: df-bi 190 df-ne 2624 |
This theorem is referenced by: necon1ai 2651 necon3i 2656 neneor 2722 disjsn2 4001 opelopabsb 4684 0nelxp 4840 fvunsn 6081 map0b 7497 mapdom3 7731 wemapso2lem 8054 cflim2 8680 isfin4-3 8732 fpwwe2lem13 9054 tskuni 9195 recextlem2 10232 hashprg 12566 eqsqrt2d 13442 gcd1 14507 gcdeq 14531 lcmfunsnlem2lem1 14622 lcmfunsnlem2lem2 14623 phimullem 14738 pcgcd1 14837 pc2dvds 14839 pockthlem 14860 ablfacrplem 17709 lbsextlem4 18395 znrrg 19147 obslbs 19304 opnfbas 20868 supfil 20921 itg1addlem4 22669 itg1addlem5 22670 dvdsmulf1o 24135 ppiub 24144 dchrelbas4 24183 lgsne0 24273 2sqlem8 24312 tgldimor 24558 nbcusgra 25203 uvtxnbgra 25233 wlkcpr 25269 vdgr1b 25644 frgraunss 25735 submateqlem1 28640 submateqlem2 28641 qqhval2 28793 derangsn 29899 subfacp1lem6 29914 cvmsss2 30003 ax6e2ndeq 36927 fperdvper 37832 dvnmul 37860 wallispi 37989 fourierdlem56 38083 gcdzeq 38884 funsndifnop 39116 |
Copyright terms: Public domain | W3C validator |