Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0ne1 | Structured version Visualization version GIF version |
Description: Zero is different from one (the commuted form is Axiom ax-1ne0 10949). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0ne1 | ⊢ 0 ≠ 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1ne0 10949 | . 2 ⊢ 1 ≠ 0 | |
2 | 1 | necomi 2999 | 1 ⊢ 0 ≠ 1 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 2944 0cc0 10880 1c1 10881 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2710 ax-1ne0 10949 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2731 df-ne 2945 |
This theorem is referenced by: f13idfv 13729 hashrabsn1 14098 prhash2ex 14123 s2f1o 14638 f1oun2prg 14639 wrdlen2i 14664 mod2eq1n2dvds 16065 bezoutr1 16283 xrsnsgrp 20643 i1f1lem 24862 mcubic 26006 cubic2 26007 asinlem 26027 sqff1o 26340 dchrpt 26424 lgsqr 26508 lgsqrmodndvds 26510 2lgslem4 26563 umgr2v2e 27901 umgr2v2evd2 27903 usgr2trlncl 28137 usgr2pthlem 28140 uspgrn2crct 28182 ntrl2v2e 28531 konigsbergiedgw 28621 konigsberglem2 28626 konigsberglem5 28629 s2f1 31228 cycpm2tr 31395 cyc3evpm 31426 indf1o 32001 eulerpartlemgf 32355 sgnpbi 32522 prodfzo03 32592 hgt750lemg 32643 hgt750lemb 32645 tgoldbachgt 32652 lcmineqlem11 40054 sn-1ne2 40302 nn0rppwr 40340 sn-inelr 40442 mncn0 40971 aaitgo 40994 fourierdlem60 43714 fourierdlem61 43715 fun2dmnopgexmpl 44787 zlmodzxzel 45702 zlmodzxzscm 45704 zlmodzxzadd 45705 zlmodzxznm 45849 zlmodzxzldeplem 45850 fv2arycl 46005 2arymptfv 46007 2arymaptf1 46010 2arymaptfo 46011 line2 46109 line2x 46111 |
Copyright terms: Public domain | W3C validator |