Theorem 0ne1 12364

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

Syntax hints:   ≠ wne 2946  0cc0 11184  1c1 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711  ax-1ne0 11253

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  f13idfv  14051  hashrabsn1  14423  prhash2ex  14448  s2f1o  14965  f1oun2prg  14966  wrdlen2i  14991  mod2eq1n2dvds  16395  nn0rppwr  16608  bezoutr1  16616  xrsnsgrp  21443  i1f1lem  25743  mcubic  26908  cubic2  26909  asinlem  26929  sqff1o  27243  dchrpt  27329  lgsqr  27413  lgsqrmodndvds  27415  2lgslem4  27468  umgr2v2e  29561  umgr2v2evd2  29563  usgr2trlncl  29796  usgr2pthlem  29799  uspgrn2crct  29841  ntrl2v2e  30190  konigsbergiedgw  30280  konigsberglem2  30285  konigsberglem5  30288  s2f1  32911  cycpm2tr  33112  cyc3evpm  33143  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  rtelextdg2lem  33717  indf1o  33988  eulerpartlemgf  34344  sgnpbi  34511  prodfzo03  34580  hgt750lemg  34631  hgt750lemb  34633  tgoldbachgt  34640  lcmineqlem11  41996  sn-1ne2  42254  expeq1d  42311  sn-nnne0  42424  sn-inelr  42443  mncn0  43096  aaitgo  43119  fourierdlem60  46087  fourierdlem61  46088  fun2dmnopgexmpl  47199  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  zlmodzxzel  48080  zlmodzxzscm  48082  zlmodzxzadd  48083  zlmodzxznm  48226  zlmodzxzldeplem  48227  fv2arycl  48382  2arymptfv  48384  2arymaptf1  48387  2arymaptfo  48388  line2  48486  line2x  48488