Theorem 0ne1 12257

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

Syntax hints:   ≠ wne 2925  0cc0 11068  1c1 11069

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 11137

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  13965  hashrabsn1  14339  prhash2ex  14364  s2f1o  14882  f1oun2prg  14883  wrdlen2i  14908  mod2eq1n2dvds  16317  nn0rppwr  16531  bezoutr1  16539  xrsnsgrp  21319  i1f1lem  25590  mcubic  26757  cubic2  26758  asinlem  26778  sqff1o  27092  dchrpt  27178  lgsqr  27262  lgsqrmodndvds  27264  2lgslem4  27317  umgr2v2e  29453  umgr2v2evd2  29455  usgr2trlncl  29690  usgr2pthlem  29693  uspgrn2crct  29738  ntrl2v2e  30087  konigsbergiedgw  30177  konigsberglem2  30182  konigsberglem5  30185  sgnpbi  32764  indf1o  32787  s2f1  32866  cycpm2tr  33076  cyc3evpm  33107  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  rtelextdg2lem  33716  eulerpartlemgf  34370  prodfzo03  34594  hgt750lemg  34645  hgt750lemb  34647  tgoldbachgt  34654  lcmineqlem11  42027  sn-1ne2  42253  expeq1d  42312  sn-nnne0  42448  sn-inelr  42475  mncn0  43128  aaitgo  43151  fourierdlem60  46164  fourierdlem61  46165  fun2dmnopgexmpl  47285  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  gpgusgralem  48047  gpgedg2ov  48057  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg3nbgrvtx1  48069  gpgprismgr4cycllem2  48086  gpgprismgr4cycllem7  48091  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  zlmodzxzel  48343  zlmodzxzscm  48345  zlmodzxzadd  48346  zlmodzxznm  48486  zlmodzxzldeplem  48487  fv2arycl  48637  2arymptfv  48639  2arymaptf1  48642  2arymaptfo  48643  line2  48741  line2x  48743