Theorem 0ne1 12199

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

Syntax hints:   ≠ wne 2925  0cc0 11009  1c1 11010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701  ax-1ne0 11078

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  f13idfv  13907  hashrabsn1  14281  prhash2ex  14306  s2f1o  14823  f1oun2prg  14824  wrdlen2i  14849  mod2eq1n2dvds  16258  nn0rppwr  16472  bezoutr1  16480  xrsnsgrp  21314  i1f1lem  25588  mcubic  26755  cubic2  26756  asinlem  26776  sqff1o  27090  dchrpt  27176  lgsqr  27260  lgsqrmodndvds  27262  2lgslem4  27315  umgr2v2e  29471  umgr2v2evd2  29473  usgr2trlncl  29705  usgr2pthlem  29708  uspgrn2crct  29753  ntrl2v2e  30102  konigsbergiedgw  30192  konigsberglem2  30197  konigsberglem5  30200  sgnpbi  32784  indf1o  32807  s2f1  32886  cycpm2tr  33061  cyc3evpm  33092  evl1deg1  33511  evl1deg2  33512  evl1deg3  33513  rtelextdg2lem  33693  eulerpartlemgf  34347  prodfzo03  34571  hgt750lemg  34622  hgt750lemb  34624  tgoldbachgt  34631  lcmineqlem11  42016  sn-1ne2  42242  expeq1d  42301  sn-nnne0  42437  sn-inelr  42464  mncn0  43116  aaitgo  43139  fourierdlem60  46151  fourierdlem61  46152  fun2dmnopgexmpl  47272  usgrexmpl1lem  48009  usgrexmpl2lem  48014  usgrexmpl2nb0  48019  gpgusgralem  48044  gpgedg2ov  48054  gpg5nbgrvtx03starlem1  48056  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem3  48061  gpg3nbgrvtx0  48064  gpg3nbgrvtx0ALT  48065  gpg3nbgrvtx1  48066  gpgprismgr4cycllem2  48084  gpgprismgr4cycllem7  48089  pgnioedg1  48096  pgnioedg2  48097  pgnioedg3  48098  pgnioedg4  48099  pgnioedg5  48100  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  zlmodzxzel  48343  zlmodzxzscm  48345  zlmodzxzadd  48346  zlmodzxznm  48486  zlmodzxzldeplem  48487  fv2arycl  48637  2arymptfv  48639  2arymaptf1  48642  2arymaptfo  48643  line2  48741  line2x  48743