Theorem 0ne1 12252

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

Syntax hints:   ≠ wne 2932  0cc0 11038  1c1 11039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708  ax-1ne0 11107

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

This theorem is referenced by:  f13idfv  13962  hashrabsn1  14336  prhash2ex  14361  s2f1o  14878  f1oun2prg  14879  wrdlen2i  14904  mod2eq1n2dvds  16316  nn0rppwr  16530  bezoutr1  16538  xrsnsgrp  21388  i1f1lem  25656  mcubic  26811  cubic2  26812  asinlem  26832  sqff1o  27145  dchrpt  27230  lgsqr  27314  lgsqrmodndvds  27316  2lgslem4  27369  umgr2v2e  29594  umgr2v2evd2  29596  usgr2trlncl  29828  usgr2pthlem  29831  uspgrn2crct  29876  ntrl2v2e  30228  konigsbergiedgw  30318  konigsberglem2  30323  konigsberglem5  30326  sgnpbi  32912  indf1o  32924  indfsid  32929  s2f1  33005  cycpm2tr  33180  cyc3evpm  33211  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  mplmulmvr  33683  rtelextdg2lem  33870  eulerpartlemgf  34523  prodfzo03  34747  hgt750lemg  34798  hgt750lemb  34800  tgoldbachgt  34807  lcmineqlem11  42478  sn-1ne2  42703  expeq1d  42756  sn-nnne0  42905  sn-inelr  42932  mncn0  43567  aaitgo  43590  fourierdlem60  46594  fourierdlem61  46595  fun2dmnopgexmpl  47732  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  gpgusgralem  48532  gpgedg2ov  48542  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem3  48549  gpg3nbgrvtx0  48552  gpg3nbgrvtx0ALT  48553  gpg3nbgrvtx1  48554  gpgprismgr4cycllem2  48572  gpgprismgr4cycllem7  48577  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  zlmodzxzel  48831  zlmodzxzscm  48833  zlmodzxzadd  48834  zlmodzxznm  48973  zlmodzxzldeplem  48974  fv2arycl  49124  2arymptfv  49126  2arymaptf1  49129  2arymaptfo  49130  line2  49228  line2x  49230