MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0ne1 Structured version   Visualization version   GIF version

Theorem 0ne1 12231
Description: Zero is different from one (the commuted form is Axiom ax-1ne0 11127). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
0ne1 0 ≠ 1

Proof of Theorem 0ne1
StepHypRef Expression
1 ax-1ne0 11127 . 2 1 ≠ 0
21necomi 2999 1 0 ≠ 1
Colors of variables: wff setvar class
Syntax hints:  wne 2944  0cc0 11058  1c1 11059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708  ax-1ne0 11127
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-ne 2945
This theorem is referenced by:  f13idfv  13912  hashrabsn1  14281  prhash2ex  14306  s2f1o  14812  f1oun2prg  14813  wrdlen2i  14838  mod2eq1n2dvds  16236  bezoutr1  16452  xrsnsgrp  20849  i1f1lem  25069  mcubic  26213  cubic2  26214  asinlem  26234  sqff1o  26547  dchrpt  26631  lgsqr  26715  lgsqrmodndvds  26717  2lgslem4  26770  umgr2v2e  28515  umgr2v2evd2  28517  usgr2trlncl  28750  usgr2pthlem  28753  uspgrn2crct  28795  ntrl2v2e  29144  konigsbergiedgw  29234  konigsberglem2  29239  konigsberglem5  29242  s2f1  31843  cycpm2tr  32010  cyc3evpm  32041  indf1o  32663  eulerpartlemgf  33019  sgnpbi  33186  prodfzo03  33256  hgt750lemg  33307  hgt750lemb  33309  tgoldbachgt  33316  lcmineqlem11  40525  sn-1ne2  40810  nn0rppwr  40848  sn-nnne0  40946  sn-inelr  40963  mncn0  41495  aaitgo  41518  fourierdlem60  44481  fourierdlem61  44482  fun2dmnopgexmpl  45590  zlmodzxzel  46505  zlmodzxzscm  46507  zlmodzxzadd  46508  zlmodzxznm  46652  zlmodzxzldeplem  46653  fv2arycl  46808  2arymptfv  46810  2arymaptf1  46813  2arymaptfo  46814  line2  46912  line2x  46914
  Copyright terms: Public domain W3C validator