Theorem 0ne1 12243

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

Syntax hints:   ≠ wne 2934  0cc0 11029  1c1 11030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711  ax-1ne0 11098

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ne 2935

This theorem is referenced by:  f13idfv  13953  hashrabsn1  14327  prhash2ex  14352  s2f1o  14869  f1oun2prg  14870  wrdlen2i  14895  mod2eq1n2dvds  16307  nn0rppwr  16521  bezoutr1  16529  xrsnsgrp  21383  i1f1lem  25674  mcubic  26829  cubic2  26830  asinlem  26850  sqff1o  27163  dchrpt  27248  lgsqr  27332  lgsqrmodndvds  27334  2lgslem4  27387  umgr2v2e  29612  umgr2v2evd2  29614  usgr2trlncl  29846  usgr2pthlem  29849  uspgrn2crct  29894  ntrl2v2e  30246  konigsbergiedgw  30336  konigsberglem2  30341  konigsberglem5  30344  sgnpbi  32931  indf1o  32943  indfsid  32948  s2f1  33024  cycpm2tr  33200  cyc3evpm  33231  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  mplmulmvr  33723  rtelextdg2lem  33910  eulerpartlemgf  34563  prodfzo03  34787  hgt750lemg  34838  hgt750lemb  34840  tgoldbachgt  34847  lcmineqlem11  42524  sn-1ne2  42748  expeq1d  42801  sn-nnne0  42950  sn-inelr  42977  mncn0  43584  aaitgo  43607  fourierdlem60  46609  fourierdlem61  46610  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