Theorem 0ne1 12053

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

Syntax hints:   ≠ wne 2944  0cc0 10880  1c1 10881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710  ax-1ne0 10949

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ne 2945

This theorem is referenced by:  f13idfv  13729  hashrabsn1  14098  prhash2ex  14123  s2f1o  14638  f1oun2prg  14639  wrdlen2i  14664  mod2eq1n2dvds  16065  bezoutr1  16283  xrsnsgrp  20643  i1f1lem  24862  mcubic  26006  cubic2  26007  asinlem  26027  sqff1o  26340  dchrpt  26424  lgsqr  26508  lgsqrmodndvds  26510  2lgslem4  26563  umgr2v2e  27901  umgr2v2evd2  27903  usgr2trlncl  28137  usgr2pthlem  28140  uspgrn2crct  28182  ntrl2v2e  28531  konigsbergiedgw  28621  konigsberglem2  28626  konigsberglem5  28629  s2f1  31228  cycpm2tr  31395  cyc3evpm  31426  indf1o  32001  eulerpartlemgf  32355  sgnpbi  32522  prodfzo03  32592  hgt750lemg  32643  hgt750lemb  32645  tgoldbachgt  32652  lcmineqlem11  40054  sn-1ne2  40302  nn0rppwr  40340  sn-inelr  40442  mncn0  40971  aaitgo  40994  fourierdlem60  43714  fourierdlem61  43715  fun2dmnopgexmpl  44787  zlmodzxzel  45702  zlmodzxzscm  45704  zlmodzxzadd  45705  zlmodzxznm  45849  zlmodzxzldeplem  45850  fv2arycl  46005  2arymptfv  46007  2arymaptf1  46010  2arymaptfo  46011  line2  46109  line2x  46111