Theorem 0ne1 12329

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

This proof depends on syntax axioms:   ≠ wne 2960  0cc0 11117  1c1 11118

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 2156  ax-ext 2737  ax-1ne0 11186

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

This theorem is used by:  f13idfv  14056  hashrabsn1  14430  prhash2ex  14455  s2f1o  14979  f1oun2prg  14980  wrdlen2i  15005  sgnpbi  15168  mod2eq1n2dvds  16429  nn0rppwr  16643  bezoutr1  16651  xrsnsgrp  21610  i1f1lem  25901  mcubic  27065  cubic2  27066  asinlem  27086  sqff1o  27399  dchrpt  27484  lgsqr  27568  lgsqrmodndvds  27570  2lgslem4  27623  umgr2v2e  29935  umgr2v2evd2  29937  usgr2trlncl  30175  usgr2pthlem  30178  uspgrn2crct  30226  ntrl2v2e  30582  konigsbergiedgw  30672  konigsberglem2  30677  konigsberglem5  30680  indf1o  33256  indfsid  33261  s2f1  33335  cycpm2tr  33505  cyc3evpm  33536  evl1deg1  33932  evl1deg2  33933  evl1deg3  33934  mplmulmvr  33995  rtelextdg2lem  34182  eulerpartlemgf  34836  prodfzo03  35057  hgt750lemg  35108  hgt750lemb  35110  tgoldbachgt  35117  lcmineqlem11  42866  sn-1ne2  43092  expeq1d  43145  sn-nnne0  43294  sn-inelr  43321  mncn0  43926  aaitgo  43949  fourierdlem60  46940  fourierdlem61  46941  fun2dmnopgexmpl  48081  usgrexmpl1lem  48846  usgrexmpl2lem  48851  usgrexmpl2nb0  48856  gpgusgralem  48881  gpgedg2ov  48891  gpg5nbgrvtx03starlem1  48893  gpg5nbgrvtx03starlem2  48894  gpg5nbgrvtx03starlem3  48895  gpg5nbgrvtx13starlem1  48896  gpg5nbgrvtx13starlem3  48898  gpg3nbgrvtx0  48901  gpg3nbgrvtx0ALT  48902  gpg3nbgrvtx1  48903  gpgprismgr4cycllem2  48921  gpgprismgr4cycllem7  48926  pgnioedg1  48933  pgnioedg2  48934  pgnioedg3  48935  pgnioedg4  48936  pgnioedg5  48937  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  zlmodzxzel  49194  zlmodzxzscm  49196  zlmodzxzadd  49197  zlmodzxznm  49336  zlmodzxzldeplem  49337  fv2arycl  49487  2arymptfv  49489  2arymaptf1  49492  2arymaptfo  49493  line2  49591  line2x  49593