Theorem 0ne1 12202

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

Syntax hints:   ≠ wne 2928  0cc0 11012  1c1 11013

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 2121  ax-ext 2703  ax-1ne0 11081

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

This theorem is referenced by:  f13idfv  13913  hashrabsn1  14287  prhash2ex  14312  s2f1o  14829  f1oun2prg  14830  wrdlen2i  14855  mod2eq1n2dvds  16264  nn0rppwr  16478  bezoutr1  16486  xrsnsgrp  21350  i1f1lem  25623  mcubic  26790  cubic2  26791  asinlem  26811  sqff1o  27125  dchrpt  27211  lgsqr  27295  lgsqrmodndvds  27297  2lgslem4  27350  umgr2v2e  29511  umgr2v2evd2  29513  usgr2trlncl  29745  usgr2pthlem  29748  uspgrn2crct  29793  ntrl2v2e  30145  konigsbergiedgw  30235  konigsberglem2  30240  konigsberglem5  30243  sgnpbi  32829  indf1o  32852  indfsid  32857  s2f1  32933  cycpm2tr  33095  cyc3evpm  33126  evl1deg1  33546  evl1deg2  33547  evl1deg3  33548  rtelextdg2lem  33746  eulerpartlemgf  34399  prodfzo03  34623  hgt750lemg  34674  hgt750lemb  34676  tgoldbachgt  34683  lcmineqlem11  42138  sn-1ne2  42364  expeq1d  42423  sn-nnne0  42559  sn-inelr  42586  mncn0  43237  aaitgo  43260  fourierdlem60  46269  fourierdlem61  46270  fun2dmnopgexmpl  47389  usgrexmpl1lem  48126  usgrexmpl2lem  48131  usgrexmpl2nb0  48136  gpgusgralem  48161  gpgedg2ov  48171  gpg5nbgrvtx03starlem1  48173  gpg5nbgrvtx03starlem2  48174  gpg5nbgrvtx03starlem3  48175  gpg5nbgrvtx13starlem1  48176  gpg5nbgrvtx13starlem3  48178  gpg3nbgrvtx0  48181  gpg3nbgrvtx0ALT  48182  gpg3nbgrvtx1  48183  gpgprismgr4cycllem2  48201  gpgprismgr4cycllem7  48206  pgnioedg1  48213  pgnioedg2  48214  pgnioedg3  48215  pgnioedg4  48216  pgnioedg5  48217  pgnbgreunbgrlem2lem1  48219  pgnbgreunbgrlem2lem2  48220  zlmodzxzel  48460  zlmodzxzscm  48462  zlmodzxzadd  48463  zlmodzxznm  48603  zlmodzxzldeplem  48604  fv2arycl  48754  2arymptfv  48756  2arymaptf1  48759  2arymaptfo  48760  line2  48858  line2x  48860