Theorem 0ne1 12337

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

Syntax hints:   ≠ wne 2940  0cc0 11155  1c1 11156

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 2007  ax-9 2118  ax-ext 2708  ax-1ne0 11224

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

This theorem is referenced by:  f13idfv  14041  hashrabsn1  14413  prhash2ex  14438  s2f1o  14955  f1oun2prg  14956  wrdlen2i  14981  mod2eq1n2dvds  16384  nn0rppwr  16598  bezoutr1  16606  xrsnsgrp  21420  i1f1lem  25724  mcubic  26890  cubic2  26891  asinlem  26911  sqff1o  27225  dchrpt  27311  lgsqr  27395  lgsqrmodndvds  27397  2lgslem4  27450  umgr2v2e  29543  umgr2v2evd2  29545  usgr2trlncl  29780  usgr2pthlem  29783  uspgrn2crct  29828  ntrl2v2e  30177  konigsbergiedgw  30267  konigsberglem2  30272  konigsberglem5  30275  indf1o  32849  s2f1  32929  cycpm2tr  33139  cyc3evpm  33170  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  rtelextdg2lem  33767  eulerpartlemgf  34381  sgnpbi  34549  prodfzo03  34618  hgt750lemg  34669  hgt750lemb  34671  tgoldbachgt  34678  lcmineqlem11  42040  sn-1ne2  42300  expeq1d  42359  sn-nnne0  42478  sn-inelr  42497  mncn0  43151  aaitgo  43174  fourierdlem60  46181  fourierdlem61  46182  fun2dmnopgexmpl  47296  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  gpgusgralem  48011  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem3  48029  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg3nbgrvtx1  48034  zlmodzxzel  48271  zlmodzxzscm  48273  zlmodzxzadd  48274  zlmodzxznm  48414  zlmodzxzldeplem  48415  fv2arycl  48569  2arymptfv  48571  2arymaptf1  48574  2arymaptfo  48575  line2  48673  line2x  48675