Theorem 0ne1 12216

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

Syntax hints:   ≠ wne 2932  0cc0 11026  1c1 11027

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 2708  ax-1ne0 11095

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

This theorem is referenced by:  f13idfv  13923  hashrabsn1  14297  prhash2ex  14322  s2f1o  14839  f1oun2prg  14840  wrdlen2i  14865  mod2eq1n2dvds  16274  nn0rppwr  16488  bezoutr1  16496  xrsnsgrp  21362  i1f1lem  25646  mcubic  26813  cubic2  26814  asinlem  26834  sqff1o  27148  dchrpt  27234  lgsqr  27318  lgsqrmodndvds  27320  2lgslem4  27373  umgr2v2e  29599  umgr2v2evd2  29601  usgr2trlncl  29833  usgr2pthlem  29836  uspgrn2crct  29881  ntrl2v2e  30233  konigsbergiedgw  30323  konigsberglem2  30328  konigsberglem5  30331  sgnpbi  32920  indf1o  32946  indfsid  32951  s2f1  33027  cycpm2tr  33201  cyc3evpm  33232  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  mplmulmvr  33704  rtelextdg2lem  33883  eulerpartlemgf  34536  prodfzo03  34760  hgt750lemg  34811  hgt750lemb  34813  tgoldbachgt  34820  lcmineqlem11  42303  sn-1ne2  42530  expeq1d  42589  sn-nnne0  42725  sn-inelr  42752  mncn0  43391  aaitgo  43414  fourierdlem60  46420  fourierdlem61  46421  fun2dmnopgexmpl  47540  usgrexmpl1lem  48277  usgrexmpl2lem  48282  usgrexmpl2nb0  48287  gpgusgralem  48312  gpgedg2ov  48322  gpg5nbgrvtx03starlem1  48324  gpg5nbgrvtx03starlem2  48325  gpg5nbgrvtx03starlem3  48326  gpg5nbgrvtx13starlem1  48327  gpg5nbgrvtx13starlem3  48329  gpg3nbgrvtx0  48332  gpg3nbgrvtx0ALT  48333  gpg3nbgrvtx1  48334  gpgprismgr4cycllem2  48352  gpgprismgr4cycllem7  48357  pgnioedg1  48364  pgnioedg2  48365  pgnioedg3  48366  pgnioedg4  48367  pgnioedg5  48368  pgnbgreunbgrlem2lem1  48370  pgnbgreunbgrlem2lem2  48371  zlmodzxzel  48611  zlmodzxzscm  48613  zlmodzxzadd  48614  zlmodzxznm  48753  zlmodzxzldeplem  48754  fv2arycl  48904  2arymptfv  48906  2arymaptf1  48909  2arymaptfo  48910  line2  49008  line2x  49010