![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0ne1 | Structured version Visualization version GIF version |
Description: 0 ≠ 1; the reverse order is already proved. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0ne1 | ⊢ 0 ≠ 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1ne0 10195 | . 2 ⊢ 1 ≠ 0 | |
2 | 1 | necomi 2984 | 1 ⊢ 0 ≠ 1 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 2930 0cc0 10126 1c1 10127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-ext 2738 ax-1ne0 10195 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1852 df-cleq 2751 df-ne 2931 |
This theorem is referenced by: f13idfv 12992 hashrabsn1 13353 prhash2ex 13377 s2f1o 13859 f1oun2prg 13860 wrdlen2i 13885 fprodn0f 14919 mod2eq1n2dvds 15271 bezoutr1 15482 xrsnsgrp 19982 i1f1lem 23653 mcubic 24771 cubic2 24772 asinlem 24792 sqff1o 25105 dchrpt 25189 lgsqr 25273 lgsqrmodndvds 25275 2lgslem4 25328 umgr2v2e 26629 umgr2v2evd2 26631 usgr2trlncl 26864 usgr2pthlem 26867 uspgrn2crct 26909 ntrl2v2e 27308 konigsbergiedgw 27398 konigsberglem2 27403 konigsberglem5 27406 nn0sqeq1 29820 indf1o 30393 eulerpartlemgf 30748 sgnpbi 30915 prodfzo03 30988 hgt750lemg 31039 hgt750lemb 31041 tgoldbachgt 31048 mncn0 38209 aaitgo 38232 fourierdlem60 40884 fourierdlem61 40885 fun2dmnopgexmpl 41809 zlmodzxzel 42641 zlmodzxzscm 42643 zlmodzxzadd 42644 zlmodzxznm 42794 zlmodzxzldeplem 42795 |
Copyright terms: Public domain | W3C validator |