Theorem 0ne1 12454

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

This proof depends on syntax axioms:   ≠ wne 2959  0cc0 11239  1c1 11240

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735  ax-1ne0 11308

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

This theorem is used by:  f13idfv  14183  hashrabsn1  14559  prhash2ex  14584  s2f1o  15110  f1oun2prg  15111  wrdlen2i  15136  sgnpbi  15301  mod2eq1n2dvds  16561  nn0rppwr  16779  bezoutr1  16788  xrsnsgrp  21766  ehl2eudis  25798  i1f1lem  26065  mcubic  27232  cubic2  27233  asinlem  27253  sqff1o  27566  dchrpt  27651  lgsqr  27735  lgsqrmodndvds  27737  2lgslem4  27790  umgr2v2e  30163  umgr2v2evd2  30165  usgr2trlncl  30403  usgr2pthlem  30406  uspgrn2crct  30454  ntrl2v2e  30816  konigsbergiedgw  30906  konigsberglem2  30911  konigsberglem5  30914  indf1o  33527  indfsid  33532  s2f1  33606  cycpm2tr  33779  cyc3evpm  33810  evl1deg1  34211  evl1deg2  34212  evl1deg3  34213  mplmulmvr  34282  rtelextdg2lem  34469  eulerpartlemgf  35122  prodfzo03  35343  hgt750lemg  35394  hgt750lemb  35396  tgoldbachgt  35403  lcmineqlem11  43355  sn-1ne2  43596  expeq1d  43647  sn-nnne0  43790  sn-inelr  43817  mncn0  44406  aaitgo  44429  fourierdlem60  47449  fourierdlem61  47450  fun2dmnopgexmpl  48627  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb0  49402  gpgusgralem  49427  gpgedg2ov  49437  gpg5nbgrvtx03starlem1  49439  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx13starlem1  49442  gpg5nbgrvtx13starlem3  49444  gpg3nbgrvtx0  49447  gpg3nbgrvtx0ALT  49448  gpg3nbgrvtx1  49449  gpgprismgr4cycllem2  49467  gpgprismgr4cycllem7  49472  pgnioedg1  49479  pgnioedg2  49480  pgnioedg3  49481  pgnioedg4  49482  pgnioedg5  49483  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  linplyfv  49711  zlmodzxzel  49798  zlmodzxzscm  49800  zlmodzxzadd  49801  zlmodzxznm  49940  zlmodzxzldeplem  49941  fv2arycl  50091  2arymptfv  50093  2arymaptf1  50096  2arymaptfo  50097  ehl2eudisval0  50169  line2  50195  line2x  50197