Theorem 0ne1 12283

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

Syntax hints:   ≠ wne 2941  0cc0 11110  1c1 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704  ax-1ne0 11179

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  f13idfv  13965  hashrabsn1  14334  prhash2ex  14359  s2f1o  14867  f1oun2prg  14868  wrdlen2i  14893  mod2eq1n2dvds  16290  bezoutr1  16506  xrsnsgrp  20981  i1f1lem  25206  mcubic  26352  cubic2  26353  asinlem  26373  sqff1o  26686  dchrpt  26770  lgsqr  26854  lgsqrmodndvds  26856  2lgslem4  26909  umgr2v2e  28782  umgr2v2evd2  28784  usgr2trlncl  29017  usgr2pthlem  29020  uspgrn2crct  29062  ntrl2v2e  29411  konigsbergiedgw  29501  konigsberglem2  29506  konigsberglem5  29509  s2f1  32111  cycpm2tr  32278  cyc3evpm  32309  indf1o  33022  eulerpartlemgf  33378  sgnpbi  33545  prodfzo03  33615  hgt750lemg  33666  hgt750lemb  33668  tgoldbachgt  33675  lcmineqlem11  40904  sn-1ne2  41179  nn0rppwr  41224  sn-nnne0  41321  sn-inelr  41338  mncn0  41881  aaitgo  41904  fourierdlem60  44882  fourierdlem61  44883  fun2dmnopgexmpl  45992  zlmodzxzel  47031  zlmodzxzscm  47033  zlmodzxzadd  47034  zlmodzxznm  47178  zlmodzxzldeplem  47179  fv2arycl  47334  2arymptfv  47336  2arymaptf1  47339  2arymaptfo  47340  line2  47438  line2x  47440