Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0ne1 | Structured version Visualization version Unicode version |
Description: (common case); the reverse order is already proved. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0ne1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1ne0 10005 | . 2 | |
2 | 1 | necomi 2848 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wne 2794 cc0 9936 c1 9937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 ax-1ne0 10005 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-ne 2795 |
This theorem is referenced by: f13idfv 12800 hashrabsn1 13163 prhash2ex 13187 s2f1o 13661 f1oun2prg 13662 wrdlen2i 13686 fprodn0f 14722 mod2eq1n2dvds 15071 bezoutr1 15282 xrsnsgrp 19782 i1f1lem 23456 mcubic 24574 cubic2 24575 asinlem 24595 sqff1o 24908 dchrpt 24992 lgsqr 25076 lgsqrmodndvds 25078 2lgslem4 25131 uvtxa01vtx 26298 umgr2v2e 26421 umgr2v2evd2 26423 usgr2trlncl 26656 usgr2pthlem 26659 uspgrn2crct 26700 ntrl2v2e 27018 konigsbergiedgw 27108 konigsberglem2 27115 konigsberglem5 27118 nn0sqeq1 29513 indf1o 30086 eulerpartlemgf 30441 sgnpbi 30608 prodfzo03 30681 hgt750lemg 30732 hgt750lemb 30734 tgoldbachgt 30741 mncn0 37709 aaitgo 37732 fourierdlem60 40383 fourierdlem61 40384 fun2dmnopgexmpl 41303 zlmodzxzel 42133 zlmodzxzscm 42135 zlmodzxzadd 42136 zlmodzxznm 42286 zlmodzxzldeplem 42287 |
Copyright terms: Public domain | W3C validator |