Theorem 0ne1 11780

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

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