Theorem 0ne1 12214

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

Syntax hints:   ≠ wne 2930  0cc0 11024  1c1 11025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706  ax-1ne0 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ne 2931

This theorem is referenced by:  f13idfv  13921  hashrabsn1  14295  prhash2ex  14320  s2f1o  14837  f1oun2prg  14838  wrdlen2i  14863  mod2eq1n2dvds  16272  nn0rppwr  16486  bezoutr1  16494  xrsnsgrp  21360  i1f1lem  25644  mcubic  26811  cubic2  26812  asinlem  26832  sqff1o  27146  dchrpt  27232  lgsqr  27316  lgsqrmodndvds  27318  2lgslem4  27371  umgr2v2e  29548  umgr2v2evd2  29550  usgr2trlncl  29782  usgr2pthlem  29785  uspgrn2crct  29830  ntrl2v2e  30182  konigsbergiedgw  30272  konigsberglem2  30277  konigsberglem5  30280  sgnpbi  32869  indf1o  32895  indfsid  32900  s2f1  32976  cycpm2tr  33150  cyc3evpm  33181  evl1deg1  33606  evl1deg2  33607  evl1deg3  33608  mplmulmvr  33653  rtelextdg2lem  33832  eulerpartlemgf  34485  prodfzo03  34709  hgt750lemg  34760  hgt750lemb  34762  tgoldbachgt  34769  lcmineqlem11  42232  sn-1ne2  42462  expeq1d  42521  sn-nnne0  42657  sn-inelr  42684  mncn0  43323  aaitgo  43346  fourierdlem60  46352  fourierdlem61  46353  fun2dmnopgexmpl  47472  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2nb0  48219  gpgusgralem  48244  gpgedg2ov  48254  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem3  48261  gpg3nbgrvtx0  48264  gpg3nbgrvtx0ALT  48265  gpg3nbgrvtx1  48266  gpgprismgr4cycllem2  48284  gpgprismgr4cycllem7  48289  pgnioedg1  48296  pgnioedg2  48297  pgnioedg3  48298  pgnioedg4  48299  pgnioedg5  48300  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  zlmodzxzel  48543  zlmodzxzscm  48545  zlmodzxzadd  48546  zlmodzxznm  48685  zlmodzxzldeplem  48686  fv2arycl  48836  2arymptfv  48838  2arymaptf1  48841  2arymaptfo  48842  line2  48940  line2x  48942