Theorem 0ne1 12337

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

This proof depends on syntax axioms:   ≠ wne 2955  0cc0 11125  1c1 11126

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732  ax-1ne0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ne 2956

This theorem is used by:  f13idfv  14065  hashrabsn1  14439  prhash2ex  14464  s2f1o  14988  f1oun2prg  14989  wrdlen2i  15014  sgnpbi  15179  mod2eq1n2dvds  16438  nn0rppwr  16652  bezoutr1  16660  xrsnsgrp  21622  i1f1lem  25918  mcubic  27085  cubic2  27086  asinlem  27106  sqff1o  27419  dchrpt  27504  lgsqr  27588  lgsqrmodndvds  27590  2lgslem4  27643  umgr2v2e  29986  umgr2v2evd2  29988  usgr2trlncl  30226  usgr2pthlem  30229  uspgrn2crct  30277  ntrl2v2e  30639  konigsbergiedgw  30729  konigsberglem2  30734  konigsberglem5  30737  indf1o  33311  indfsid  33316  s2f1  33390  cycpm2tr  33560  cyc3evpm  33591  evl1deg1  33987  evl1deg2  33988  evl1deg3  33989  mplmulmvr  34050  rtelextdg2lem  34237  eulerpartlemgf  34891  prodfzo03  35112  hgt750lemg  35163  hgt750lemb  35165  tgoldbachgt  35172  lcmineqlem11  42906  sn-1ne2  43147  expeq1d  43200  sn-nnne0  43349  sn-inelr  43376  mncn0  43981  aaitgo  44004  fourierdlem60  46995  fourierdlem61  46996  fun2dmnopgexmpl  48173  usgrexmpl1lem  48938  usgrexmpl2lem  48943  usgrexmpl2nb0  48948  gpgusgralem  48973  gpgedg2ov  48983  gpg5nbgrvtx03starlem1  48985  gpg5nbgrvtx03starlem2  48986  gpg5nbgrvtx03starlem3  48987  gpg5nbgrvtx13starlem1  48988  gpg5nbgrvtx13starlem3  48990  gpg3nbgrvtx0  48993  gpg3nbgrvtx0ALT  48994  gpg3nbgrvtx1  48995  gpgprismgr4cycllem2  49013  gpgprismgr4cycllem7  49018  pgnioedg1  49025  pgnioedg2  49026  pgnioedg3  49027  pgnioedg4  49028  pgnioedg5  49029  pgnbgreunbgrlem2lem1  49031  pgnbgreunbgrlem2lem2  49032  zlmodzxzel  49286  zlmodzxzscm  49288  zlmodzxzadd  49289  zlmodzxznm  49428  zlmodzxzldeplem  49429  fv2arycl  49579  2arymptfv  49581  2arymaptf1  49584  2arymaptfo  49585  line2  49683  line2x  49685