Theorem 0ne1 12289

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

Syntax hints:   ≠ wne 2957  0cc0 11073  1c1 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734  ax-1ne0 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ne 2958

This theorem is referenced by:  f13idfv  14013  hashrabsn1  14387  prhash2ex  14412  s2f1o  14929  f1oun2prg  14930  wrdlen2i  14955  sgnpbi  15118  mod2eq1n2dvds  16381  nn0rppwr  16595  bezoutr1  16603  xrsnsgrp  21460  i1f1lem  25751  mcubic  26912  cubic2  26913  asinlem  26933  sqff1o  27246  dchrpt  27331  lgsqr  27415  lgsqrmodndvds  27417  2lgslem4  27470  umgr2v2e  29726  umgr2v2evd2  29728  usgr2trlncl  29960  usgr2pthlem  29963  uspgrn2crct  30008  ntrl2v2e  30360  konigsbergiedgw  30450  konigsberglem2  30455  konigsberglem5  30458  indf1o  33042  indfsid  33047  s2f1  33123  cycpm2tr  33299  cyc3evpm  33330  evl1deg1  33772  evl1deg2  33773  evl1deg3  33774  mplmulmvr  33836  rtelextdg2lem  34023  eulerpartlemgf  34676  prodfzo03  34897  hgt750lemg  34948  hgt750lemb  34950  tgoldbachgt  34957  lcmineqlem11  42656  sn-1ne2  42880  expeq1d  42933  sn-nnne0  43082  sn-inelr  43109  mncn0  43716  aaitgo  43739  fourierdlem60  46740  fourierdlem61  46741  fun2dmnopgexmpl  47878  usgrexmpl1lem  48643  usgrexmpl2lem  48648  usgrexmpl2nb0  48653  gpgusgralem  48678  gpgedg2ov  48688  gpg5nbgrvtx03starlem1  48690  gpg5nbgrvtx03starlem2  48691  gpg5nbgrvtx03starlem3  48692  gpg5nbgrvtx13starlem1  48693  gpg5nbgrvtx13starlem3  48695  gpg3nbgrvtx0  48698  gpg3nbgrvtx0ALT  48699  gpg3nbgrvtx1  48700  gpgprismgr4cycllem2  48718  gpgprismgr4cycllem7  48723  pgnioedg1  48730  pgnioedg2  48731  pgnioedg3  48732  pgnioedg4  48733  pgnioedg5  48734  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  zlmodzxzel  48977  zlmodzxzscm  48979  zlmodzxzadd  48980  zlmodzxznm  49119  zlmodzxzldeplem  49120  fv2arycl  49270  2arymptfv  49272  2arymaptf1  49275  2arymaptfo  49276  line2  49374  line2x  49376