Theorem 0ne1 12307

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

Syntax hints:   ≠ wne 2958  0cc0 11095  1c1 11096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735  ax-1ne0 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  f13idfv  14032  hashrabsn1  14406  prhash2ex  14431  s2f1o  14949  f1oun2prg  14950  wrdlen2i  14975  sgnpbi  15138  mod2eq1n2dvds  16400  nn0rppwr  16614  bezoutr1  16622  xrsnsgrp  21558  i1f1lem  25848  mcubic  27012  cubic2  27013  asinlem  27033  sqff1o  27346  dchrpt  27431  lgsqr  27515  lgsqrmodndvds  27517  2lgslem4  27570  umgr2v2e  29875  umgr2v2evd2  29877  usgr2trlncl  30109  usgr2pthlem  30112  uspgrn2crct  30157  ntrl2v2e  30509  konigsbergiedgw  30599  konigsberglem2  30604  konigsberglem5  30607  indf1o  33184  indfsid  33189  s2f1  33265  cycpm2tr  33439  cyc3evpm  33470  evl1deg1  33866  evl1deg2  33867  evl1deg3  33868  mplmulmvr  33929  rtelextdg2lem  34116  eulerpartlemgf  34769  prodfzo03  34990  hgt750lemg  35041  hgt750lemb  35043  tgoldbachgt  35050  lcmineqlem11  42826  sn-1ne2  43052  expeq1d  43105  sn-nnne0  43254  sn-inelr  43281  mncn0  43886  aaitgo  43909  fourierdlem60  46900  fourierdlem61  46901  fun2dmnopgexmpl  48041  usgrexmpl1lem  48806  usgrexmpl2lem  48811  usgrexmpl2nb0  48816  gpgusgralem  48841  gpgedg2ov  48851  gpg5nbgrvtx03starlem1  48853  gpg5nbgrvtx03starlem2  48854  gpg5nbgrvtx03starlem3  48855  gpg5nbgrvtx13starlem1  48856  gpg5nbgrvtx13starlem3  48858  gpg3nbgrvtx0  48861  gpg3nbgrvtx0ALT  48862  gpg3nbgrvtx1  48863  gpgprismgr4cycllem2  48881  gpgprismgr4cycllem7  48886  pgnioedg1  48893  pgnioedg2  48894  pgnioedg3  48895  pgnioedg4  48896  pgnioedg5  48897  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  zlmodzxzel  49155  zlmodzxzscm  49157  zlmodzxzadd  49158  zlmodzxznm  49297  zlmodzxzldeplem  49298  fv2arycl  49448  2arymptfv  49450  2arymaptf1  49453  2arymaptfo  49454  line2  49552  line2x  49554