Theorem 0ne1 12414

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

This proof depends on syntax axioms:   ≠ wne 2956  0cc0 11200  1c1 11201

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733  ax-1ne0 11269

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  f13idfv  14143  hashrabsn1  14518  prhash2ex  14543  s2f1o  15067  f1oun2prg  15068  wrdlen2i  15093  sgnpbi  15258  mod2eq1n2dvds  16517  nn0rppwr  16735  bezoutr1  16744  xrsnsgrp  21714  i1f1lem  26010  mcubic  27175  cubic2  27176  asinlem  27196  sqff1o  27509  dchrpt  27594  lgsqr  27678  lgsqrmodndvds  27680  2lgslem4  27733  umgr2v2e  30106  umgr2v2evd2  30108  usgr2trlncl  30346  usgr2pthlem  30349  uspgrn2crct  30397  ntrl2v2e  30759  konigsbergiedgw  30849  konigsberglem2  30854  konigsberglem5  30857  indf1o  33431  indfsid  33436  s2f1  33510  cycpm2tr  33680  cyc3evpm  33711  evl1deg1  34108  evl1deg2  34109  evl1deg3  34110  mplmulmvr  34171  rtelextdg2lem  34358  eulerpartlemgf  35011  prodfzo03  35232  hgt750lemg  35283  hgt750lemb  35285  tgoldbachgt  35292  lcmineqlem11  43089  sn-1ne2  43330  expeq1d  43381  sn-nnne0  43524  sn-inelr  43551  mncn0  44140  aaitgo  44163  fourierdlem60  47175  fourierdlem61  47176  fun2dmnopgexmpl  48353  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb0  49128  gpgusgralem  49153  gpgedg2ov  49163  gpg5nbgrvtx03starlem1  49165  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx03starlem3  49167  gpg5nbgrvtx13starlem1  49168  gpg5nbgrvtx13starlem3  49170  gpg3nbgrvtx0  49173  gpg3nbgrvtx0ALT  49174  gpg3nbgrvtx1  49175  gpgprismgr4cycllem2  49193  gpgprismgr4cycllem7  49198  pgnioedg1  49205  pgnioedg2  49206  pgnioedg3  49207  pgnioedg4  49208  pgnioedg5  49209  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  zlmodzxzel  49466  zlmodzxzscm  49468  zlmodzxzadd  49469  zlmodzxznm  49608  zlmodzxzldeplem  49609  fv2arycl  49759  2arymptfv  49761  2arymaptf1  49764  2arymaptfo  49765  line2  49863  line2x  49865