Theorem 0ne1 12424

Description: Zero is different from one (the commuted form is Axiom ax-1ne0 11279). (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 11279	. 2 ⊢ 1 ≠ 0
2	1	necomi 3012	1 ⊢ 0 ≠ 1

This proof depends on syntax axioms:   ≠ wne 2958  0cc0 11210  1c1 11211

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735  ax-1ne0 11279

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ne 2959

This theorem is used by:  f13idfv  14153  hashrabsn1  14528  prhash2ex  14553  s2f1o  15079  f1oun2prg  15080  wrdlen2i  15105  sgnpbi  15270  mod2eq1n2dvds  16529  nn0rppwr  16747  bezoutr1  16756  xrsnsgrp  21726  ehl2eudis  25755  i1f1lem  26022  mcubic  27187  cubic2  27188  asinlem  27208  sqff1o  27521  dchrpt  27606  lgsqr  27690  lgsqrmodndvds  27692  2lgslem4  27745  umgr2v2e  30118  umgr2v2evd2  30120  usgr2trlncl  30358  usgr2pthlem  30361  uspgrn2crct  30409  ntrl2v2e  30771  konigsbergiedgw  30861  konigsberglem2  30866  konigsberglem5  30869  indf1o  33484  indfsid  33489  s2f1  33563  cycpm2tr  33733  cyc3evpm  33764  evl1deg1  34161  evl1deg2  34162  evl1deg3  34163  mplmulmvr  34224  rtelextdg2lem  34411  eulerpartlemgf  35064  prodfzo03  35285  hgt750lemg  35336  hgt750lemb  35338  tgoldbachgt  35345  lcmineqlem11  43229  sn-1ne2  43470  expeq1d  43521  sn-nnne0  43664  sn-inelr  43691  mncn0  44281  aaitgo  44304  fourierdlem60  47315  fourierdlem61  47316  fun2dmnopgexmpl  48493  usgrexmpl1lem  49258  usgrexmpl2lem  49263  usgrexmpl2nb0  49268  gpgusgralem  49293  gpgedg2ov  49303  gpg5nbgrvtx03starlem1  49305  gpg5nbgrvtx03starlem2  49306  gpg5nbgrvtx03starlem3  49307  gpg5nbgrvtx13starlem1  49308  gpg5nbgrvtx13starlem3  49310  gpg3nbgrvtx0  49313  gpg3nbgrvtx0ALT  49314  gpg3nbgrvtx1  49315  gpgprismgr4cycllem2  49333  gpgprismgr4cycllem7  49338  pgnioedg1  49345  pgnioedg2  49346  pgnioedg3  49347  pgnioedg4  49348  pgnioedg5  49349  pgnbgreunbgrlem2lem1  49351  pgnbgreunbgrlem2lem2  49352  zlmodzxzel  49606  zlmodzxzscm  49608  zlmodzxzadd  49609  zlmodzxznm  49748  zlmodzxzldeplem  49749  fv2arycl  49899  2arymptfv  49901  2arymaptf1  49904  2arymaptfo  49905  ehl2eudisval0  49977  line2  50003  line2x  50005