Theorem 0ne1 12334

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

Syntax hints:   ≠ wne 2937  0cc0 11152  1c1 11153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705  ax-1ne0 11221

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  f13idfv  14037  hashrabsn1  14409  prhash2ex  14434  s2f1o  14951  f1oun2prg  14952  wrdlen2i  14977  mod2eq1n2dvds  16380  nn0rppwr  16594  bezoutr1  16602  xrsnsgrp  21437  i1f1lem  25737  mcubic  26904  cubic2  26905  asinlem  26925  sqff1o  27239  dchrpt  27325  lgsqr  27409  lgsqrmodndvds  27411  2lgslem4  27464  umgr2v2e  29557  umgr2v2evd2  29559  usgr2trlncl  29792  usgr2pthlem  29795  uspgrn2crct  29837  ntrl2v2e  30186  konigsbergiedgw  30276  konigsberglem2  30281  konigsberglem5  30284  s2f1  32913  cycpm2tr  33121  cyc3evpm  33152  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  rtelextdg2lem  33731  indf1o  34004  eulerpartlemgf  34360  sgnpbi  34527  prodfzo03  34596  hgt750lemg  34647  hgt750lemb  34649  tgoldbachgt  34656  lcmineqlem11  42020  sn-1ne2  42278  expeq1d  42337  sn-nnne0  42454  sn-inelr  42473  mncn0  43127  aaitgo  43150  fourierdlem60  46121  fourierdlem61  46122  fun2dmnopgexmpl  47233  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb0  47925  gpgusgralem  47945  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  zlmodzxzel  48199  zlmodzxzscm  48201  zlmodzxzadd  48202  zlmodzxznm  48342  zlmodzxzldeplem  48343  fv2arycl  48497  2arymptfv  48499  2arymaptf1  48502  2arymaptfo  48503  line2  48601  line2x  48603