Theorem 0ne1 12233

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

Syntax hints:   ≠ wne 2925  0cc0 11044  1c1 11045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701  ax-1ne0 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  f13idfv  13941  hashrabsn1  14315  prhash2ex  14340  s2f1o  14858  f1oun2prg  14859  wrdlen2i  14884  mod2eq1n2dvds  16293  nn0rppwr  16507  bezoutr1  16515  xrsnsgrp  21349  i1f1lem  25623  mcubic  26790  cubic2  26791  asinlem  26811  sqff1o  27125  dchrpt  27211  lgsqr  27295  lgsqrmodndvds  27297  2lgslem4  27350  umgr2v2e  29506  umgr2v2evd2  29508  usgr2trlncl  29740  usgr2pthlem  29743  uspgrn2crct  29788  ntrl2v2e  30137  konigsbergiedgw  30227  konigsberglem2  30232  konigsberglem5  30235  sgnpbi  32814  indf1o  32837  s2f1  32916  cycpm2tr  33091  cyc3evpm  33122  evl1deg1  33538  evl1deg2  33539  evl1deg3  33540  rtelextdg2lem  33709  eulerpartlemgf  34363  prodfzo03  34587  hgt750lemg  34638  hgt750lemb  34640  tgoldbachgt  34647  lcmineqlem11  42020  sn-1ne2  42246  expeq1d  42305  sn-nnne0  42441  sn-inelr  42468  mncn0  43121  aaitgo  43144  fourierdlem60  46157  fourierdlem61  46158  fun2dmnopgexmpl  47278  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb0  48015  gpgusgralem  48040  gpgedg2ov  48050  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem3  48057  gpg3nbgrvtx0  48060  gpg3nbgrvtx0ALT  48061  gpg3nbgrvtx1  48062  gpgprismgr4cycllem2  48079  gpgprismgr4cycllem7  48084  pgnioedg1  48091  pgnioedg2  48092  pgnioedg3  48093  pgnioedg4  48094  pgnioedg5  48095  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  zlmodzxzel  48336  zlmodzxzscm  48338  zlmodzxzadd  48339  zlmodzxznm  48479  zlmodzxzldeplem  48480  fv2arycl  48630  2arymptfv  48632  2arymaptf1  48635  2arymaptfo  48636  line2  48734  line2x  48736