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 10677). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0ne1 | ⊢ 0 ≠ 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1ne0 10677 | . 2 ⊢ 1 ≠ 0 | |
2 | 1 | necomi 2988 | 1 ⊢ 0 ≠ 1 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 2934 0cc0 10608 1c1 10609 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-9 2123 ax-ext 2710 ax-1ne0 10677 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-cleq 2730 df-ne 2935 |
This theorem is referenced by: f13idfv 13452 hashrabsn1 13820 prhash2ex 13845 s2f1o 14360 f1oun2prg 14361 wrdlen2i 14386 mod2eq1n2dvds 15785 bezoutr1 16003 xrsnsgrp 20246 i1f1lem 24434 mcubic 25577 cubic2 25578 asinlem 25598 sqff1o 25911 dchrpt 25995 lgsqr 26079 lgsqrmodndvds 26081 2lgslem4 26134 umgr2v2e 27459 umgr2v2evd2 27461 usgr2trlncl 27693 usgr2pthlem 27696 uspgrn2crct 27738 ntrl2v2e 28087 konigsbergiedgw 28177 konigsberglem2 28182 konigsberglem5 28185 s2f1 30786 cycpm2tr 30955 cyc3evpm 30986 indf1o 31554 eulerpartlemgf 31908 sgnpbi 32075 prodfzo03 32145 hgt750lemg 32196 hgt750lemb 32198 tgoldbachgt 32205 lcmineqlem11 39656 sn-1ne2 39855 nn0rppwr 39894 sn-inelr 39996 mncn0 40520 aaitgo 40543 fourierdlem60 43233 fourierdlem61 43234 fun2dmnopgexmpl 44293 zlmodzxzel 45209 zlmodzxzscm 45211 zlmodzxzadd 45212 zlmodzxznm 45356 zlmodzxzldeplem 45357 fv2arycl 45512 2arymptfv 45514 2arymaptf1 45517 2arymaptfo 45518 line2 45616 line2x 45618 |
Copyright terms: Public domain | W3C validator |