Theorem 0ne1 12312

Description: Zero is different from one (the commuted form is Axiom ax-1ne0 11169). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0ne1	⊢ 0 ≠ 1

Proof of Theorem 0ne1

Step	Hyp	Ref	Expression
1		ax-1ne0 11169	. 2 ⊢ 1 ≠ 0
2	1	necomi 3018	1 ⊢ 0 ≠ 1

Syntax hints:   ≠ wne 2964  0cc0 11100  1c1 11101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741  ax-1ne0 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  f13idfv  14036  hashrabsn1  14410  prhash2ex  14435  s2f1o  14953  f1oun2prg  14954  wrdlen2i  14979  sgnpbi  15142  mod2eq1n2dvds  16405  nn0rppwr  16619  bezoutr1  16627  xrsnsgrp  21527  i1f1lem  25817  mcubic  26978  cubic2  26979  asinlem  26999  sqff1o  27312  dchrpt  27397  lgsqr  27481  lgsqrmodndvds  27483  2lgslem4  27536  umgr2v2e  29816  umgr2v2evd2  29818  usgr2trlncl  30050  usgr2pthlem  30053  uspgrn2crct  30098  ntrl2v2e  30450  konigsbergiedgw  30540  konigsberglem2  30545  konigsberglem5  30548  indf1o  33125  indfsid  33130  s2f1  33206  cycpm2tr  33380  cyc3evpm  33411  evl1deg1  33811  evl1deg2  33812  evl1deg3  33813  mplmulmvr  33874  rtelextdg2lem  34061  eulerpartlemgf  34714  prodfzo03  34935  hgt750lemg  34986  hgt750lemb  34988  tgoldbachgt  34995  lcmineqlem11  42696  sn-1ne2  42922  expeq1d  42975  sn-nnne0  43124  sn-inelr  43151  mncn0  43758  aaitgo  43781  fourierdlem60  46772  fourierdlem61  46773  fun2dmnopgexmpl  47910  usgrexmpl1lem  48675  usgrexmpl2lem  48680  usgrexmpl2nb0  48685  gpgusgralem  48710  gpgedg2ov  48720  gpg5nbgrvtx03starlem1  48722  gpg5nbgrvtx03starlem2  48723  gpg5nbgrvtx03starlem3  48724  gpg5nbgrvtx13starlem1  48725  gpg5nbgrvtx13starlem3  48727  gpg3nbgrvtx0  48730  gpg3nbgrvtx0ALT  48731  gpg3nbgrvtx1  48732  gpgprismgr4cycllem2  48750  gpgprismgr4cycllem7  48755  pgnioedg1  48762  pgnioedg2  48763  pgnioedg3  48764  pgnioedg4  48765  pgnioedg5  48766  pgnbgreunbgrlem2lem1  48768  pgnbgreunbgrlem2lem2  48769  zlmodzxzel  49020  zlmodzxzscm  49022  zlmodzxzadd  49023  zlmodzxznm  49162  zlmodzxzldeplem  49163  fv2arycl  49313  2arymptfv  49315  2arymaptf1  49318  2arymaptfo  49319  line2  49417  line2x  49419