Theorem 0ne1 12314

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

Syntax hints:   ≠ wne 2964  0cc0 11102  1c1 11103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741  ax-1ne0 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  f13idfv  14038  hashrabsn1  14412  prhash2ex  14437  s2f1o  14955  f1oun2prg  14956  wrdlen2i  14981  sgnpbi  15144  mod2eq1n2dvds  16407  nn0rppwr  16621  bezoutr1  16629  xrsnsgrp  21529  i1f1lem  25819  mcubic  26980  cubic2  26981  asinlem  27001  sqff1o  27314  dchrpt  27399  lgsqr  27483  lgsqrmodndvds  27485  2lgslem4  27538  umgr2v2e  29818  umgr2v2evd2  29820  usgr2trlncl  30052  usgr2pthlem  30055  uspgrn2crct  30100  ntrl2v2e  30452  konigsbergiedgw  30542  konigsberglem2  30547  konigsberglem5  30550  indf1o  33127  indfsid  33132  s2f1  33208  cycpm2tr  33382  cyc3evpm  33413  evl1deg1  33813  evl1deg2  33814  evl1deg3  33815  mplmulmvr  33876  rtelextdg2lem  34063  eulerpartlemgf  34716  prodfzo03  34937  hgt750lemg  34988  hgt750lemb  34990  tgoldbachgt  34997  lcmineqlem11  42733  sn-1ne2  42959  expeq1d  43012  sn-nnne0  43161  sn-inelr  43188  mncn0  43795  aaitgo  43818  fourierdlem60  46809  fourierdlem61  46810  fun2dmnopgexmpl  47947  usgrexmpl1lem  48712  usgrexmpl2lem  48717  usgrexmpl2nb0  48722  gpgusgralem  48747  gpgedg2ov  48757  gpg5nbgrvtx03starlem1  48759  gpg5nbgrvtx03starlem2  48760  gpg5nbgrvtx03starlem3  48761  gpg5nbgrvtx13starlem1  48762  gpg5nbgrvtx13starlem3  48764  gpg3nbgrvtx0  48767  gpg3nbgrvtx0ALT  48768  gpg3nbgrvtx1  48769  gpgprismgr4cycllem2  48787  gpgprismgr4cycllem7  48792  pgnioedg1  48799  pgnioedg2  48800  pgnioedg3  48801  pgnioedg4  48802  pgnioedg5  48803  pgnbgreunbgrlem2lem1  48805  pgnbgreunbgrlem2lem2  48806  zlmodzxzel  49057  zlmodzxzscm  49059  zlmodzxzadd  49060  zlmodzxznm  49199  zlmodzxzldeplem  49200  fv2arycl  49350  2arymptfv  49352  2arymaptf1  49355  2arymaptfo  49356  line2  49454  line2x  49456