Theorem 0ne1 12311

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

Syntax hints:   ≠ wne 2932  0cc0 11129  1c1 11130

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 2007  ax-9 2118  ax-ext 2707  ax-1ne0 11198

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ne 2933

This theorem is referenced by:  f13idfv  14018  hashrabsn1  14392  prhash2ex  14417  s2f1o  14935  f1oun2prg  14936  wrdlen2i  14961  mod2eq1n2dvds  16366  nn0rppwr  16580  bezoutr1  16588  xrsnsgrp  21370  i1f1lem  25642  mcubic  26809  cubic2  26810  asinlem  26830  sqff1o  27144  dchrpt  27230  lgsqr  27314  lgsqrmodndvds  27316  2lgslem4  27369  umgr2v2e  29505  umgr2v2evd2  29507  usgr2trlncl  29742  usgr2pthlem  29745  uspgrn2crct  29790  ntrl2v2e  30139  konigsbergiedgw  30229  konigsberglem2  30234  konigsberglem5  30237  sgnpbi  32818  indf1o  32841  s2f1  32920  cycpm2tr  33130  cyc3evpm  33161  evl1deg1  33589  evl1deg2  33590  evl1deg3  33591  rtelextdg2lem  33760  eulerpartlemgf  34411  prodfzo03  34635  hgt750lemg  34686  hgt750lemb  34688  tgoldbachgt  34695  lcmineqlem11  42052  sn-1ne2  42315  expeq1d  42373  sn-nnne0  42491  sn-inelr  42510  mncn0  43163  aaitgo  43186  fourierdlem60  46195  fourierdlem61  46196  fun2dmnopgexmpl  47313  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2nb0  48035  gpgusgralem  48060  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem3  48075  gpg3nbgrvtx0  48078  gpg3nbgrvtx0ALT  48079  gpg3nbgrvtx1  48080  gpgprismgr4cycllem2  48095  gpgprismgr4cycllem7  48100  zlmodzxzel  48330  zlmodzxzscm  48332  zlmodzxzadd  48333  zlmodzxznm  48473  zlmodzxzldeplem  48474  fv2arycl  48628  2arymptfv  48630  2arymaptf1  48633  2arymaptfo  48634  line2  48732  line2x  48734