Theorem 0ne1 11974

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

Syntax hints:   ≠ wne 2942  0cc0 10802  1c1 10803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709  ax-1ne0 10871

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  f13idfv  13648  hashrabsn1  14017  prhash2ex  14042  s2f1o  14557  f1oun2prg  14558  wrdlen2i  14583  mod2eq1n2dvds  15984  bezoutr1  16202  xrsnsgrp  20546  i1f1lem  24758  mcubic  25902  cubic2  25903  asinlem  25923  sqff1o  26236  dchrpt  26320  lgsqr  26404  lgsqrmodndvds  26406  2lgslem4  26459  umgr2v2e  27795  umgr2v2evd2  27797  usgr2trlncl  28029  usgr2pthlem  28032  uspgrn2crct  28074  ntrl2v2e  28423  konigsbergiedgw  28513  konigsberglem2  28518  konigsberglem5  28521  s2f1  31121  cycpm2tr  31288  cyc3evpm  31319  indf1o  31892  eulerpartlemgf  32246  sgnpbi  32413  prodfzo03  32483  hgt750lemg  32534  hgt750lemb  32536  tgoldbachgt  32543  lcmineqlem11  39975  sn-1ne2  40216  nn0rppwr  40254  sn-inelr  40356  mncn0  40880  aaitgo  40903  fourierdlem60  43597  fourierdlem61  43598  fun2dmnopgexmpl  44663  zlmodzxzel  45579  zlmodzxzscm  45581  zlmodzxzadd  45582  zlmodzxznm  45726  zlmodzxzldeplem  45727  fv2arycl  45882  2arymptfv  45884  2arymaptf1  45887  2arymaptfo  45888  line2  45986  line2x  45988