Theorem 0ne1 12246

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

Syntax hints:   ≠ wne 2933  0cc0 11032  1c1 11033

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709  ax-1ne0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  f13idfv  13956  hashrabsn1  14330  prhash2ex  14355  s2f1o  14872  f1oun2prg  14873  wrdlen2i  14898  mod2eq1n2dvds  16310  nn0rppwr  16524  bezoutr1  16532  xrsnsgrp  21400  i1f1lem  25669  mcubic  26827  cubic2  26828  asinlem  26848  sqff1o  27162  dchrpt  27247  lgsqr  27331  lgsqrmodndvds  27333  2lgslem4  27386  umgr2v2e  29612  umgr2v2evd2  29614  usgr2trlncl  29846  usgr2pthlem  29849  uspgrn2crct  29894  ntrl2v2e  30246  konigsbergiedgw  30336  konigsberglem2  30341  konigsberglem5  30344  sgnpbi  32930  indf1o  32942  indfsid  32947  s2f1  33023  cycpm2tr  33198  cyc3evpm  33229  evl1deg1  33654  evl1deg2  33655  evl1deg3  33656  mplmulmvr  33701  rtelextdg2lem  33889  eulerpartlemgf  34542  prodfzo03  34766  hgt750lemg  34817  hgt750lemb  34819  tgoldbachgt  34826  lcmineqlem11  42495  sn-1ne2  42720  expeq1d  42773  sn-nnne0  42922  sn-inelr  42949  mncn0  43588  aaitgo  43611  fourierdlem60  46615  fourierdlem61  46616  fun2dmnopgexmpl  47747  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb0  48522  gpgusgralem  48547  gpgedg2ov  48557  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem3  48564  gpg3nbgrvtx0  48567  gpg3nbgrvtx0ALT  48568  gpg3nbgrvtx1  48569  gpgprismgr4cycllem2  48587  gpgprismgr4cycllem7  48592  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  zlmodzxzel  48846  zlmodzxzscm  48848  zlmodzxzadd  48849  zlmodzxznm  48988  zlmodzxzldeplem  48989  fv2arycl  49139  2arymptfv  49141  2arymaptf1  49144  2arymaptfo  49145  line2  49243  line2x  49245