Theorem 0ne1 12233

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

Syntax hints:   ≠ wne 2939  0cc0 11060  1c1 11061

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702  ax-1ne0 11129

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ne 2940

This theorem is referenced by:  f13idfv  13915  hashrabsn1  14284  prhash2ex  14309  s2f1o  14817  f1oun2prg  14818  wrdlen2i  14843  mod2eq1n2dvds  16240  bezoutr1  16456  xrsnsgrp  20870  i1f1lem  25090  mcubic  26234  cubic2  26235  asinlem  26255  sqff1o  26568  dchrpt  26652  lgsqr  26736  lgsqrmodndvds  26738  2lgslem4  26791  umgr2v2e  28536  umgr2v2evd2  28538  usgr2trlncl  28771  usgr2pthlem  28774  uspgrn2crct  28816  ntrl2v2e  29165  konigsbergiedgw  29255  konigsberglem2  29260  konigsberglem5  29263  s2f1  31871  cycpm2tr  32038  cyc3evpm  32069  indf1o  32712  eulerpartlemgf  33068  sgnpbi  33235  prodfzo03  33305  hgt750lemg  33356  hgt750lemb  33358  tgoldbachgt  33365  lcmineqlem11  40569  sn-1ne2  40839  nn0rppwr  40877  sn-nnne0  40975  sn-inelr  40992  mncn0  41524  aaitgo  41547  fourierdlem60  44527  fourierdlem61  44528  fun2dmnopgexmpl  45636  zlmodzxzel  46551  zlmodzxzscm  46553  zlmodzxzadd  46554  zlmodzxznm  46698  zlmodzxzldeplem  46699  fv2arycl  46854  2arymptfv  46856  2arymaptf1  46859  2arymaptfo  46860  line2  46958  line2x  46960