Theorem 0ne1 12228

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

Syntax hints:   ≠ wne 2933  0cc0 11038  1c1 11039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709  ax-1ne0 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  f13idfv  13935  hashrabsn1  14309  prhash2ex  14334  s2f1o  14851  f1oun2prg  14852  wrdlen2i  14877  mod2eq1n2dvds  16286  nn0rppwr  16500  bezoutr1  16508  xrsnsgrp  21374  i1f1lem  25658  mcubic  26825  cubic2  26826  asinlem  26846  sqff1o  27160  dchrpt  27246  lgsqr  27330  lgsqrmodndvds  27332  2lgslem4  27385  umgr2v2e  29611  umgr2v2evd2  29613  usgr2trlncl  29845  usgr2pthlem  29848  uspgrn2crct  29893  ntrl2v2e  30245  konigsbergiedgw  30335  konigsberglem2  30340  konigsberglem5  30343  sgnpbi  32931  indf1o  32957  indfsid  32962  s2f1  33038  cycpm2tr  33213  cyc3evpm  33244  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  mplmulmvr  33716  rtelextdg2lem  33904  eulerpartlemgf  34557  prodfzo03  34781  hgt750lemg  34832  hgt750lemb  34834  tgoldbachgt  34841  lcmineqlem11  42409  sn-1ne2  42635  expeq1d  42694  sn-nnne0  42830  sn-inelr  42857  mncn0  43496  aaitgo  43519  fourierdlem60  46524  fourierdlem61  46525  fun2dmnopgexmpl  47644  usgrexmpl1lem  48381  usgrexmpl2lem  48386  usgrexmpl2nb0  48391  gpgusgralem  48416  gpgedg2ov  48426  gpg5nbgrvtx03starlem1  48428  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx03starlem3  48430  gpg5nbgrvtx13starlem1  48431  gpg5nbgrvtx13starlem3  48433  gpg3nbgrvtx0  48436  gpg3nbgrvtx0ALT  48437  gpg3nbgrvtx1  48438  gpgprismgr4cycllem2  48456  gpgprismgr4cycllem7  48461  pgnioedg1  48468  pgnioedg2  48469  pgnioedg3  48470  pgnioedg4  48471  pgnioedg5  48472  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  zlmodzxzel  48715  zlmodzxzscm  48717  zlmodzxzadd  48718  zlmodzxznm  48857  zlmodzxzldeplem  48858  fv2arycl  49008  2arymptfv  49010  2arymaptf1  49013  2arymaptfo  49014  line2  49112  line2x  49114