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

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

Proof of Theorem 0ne1
StepHypRef Expression
1 ax-1ne0 10605 . 2 1 ≠ 0
21necomi 3070 1 0 ≠ 1
Colors of variables: wff setvar class
Syntax hints:  wne 3016  0cc0 10536  1c1 10537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793  ax-1ne0 10605
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017
This theorem is referenced by:  f13idfv  13367  hashrabsn1  13734  prhash2ex  13759  s2f1o  14277  f1oun2prg  14278  wrdlen2i  14303  mod2eq1n2dvds  15695  bezoutr1  15912  xrsnsgrp  20580  i1f1lem  24289  mcubic  25424  cubic2  25425  asinlem  25445  sqff1o  25758  dchrpt  25842  lgsqr  25926  lgsqrmodndvds  25928  2lgslem4  25981  umgr2v2e  27306  umgr2v2evd2  27308  usgr2trlncl  27540  usgr2pthlem  27543  uspgrn2crct  27585  ntrl2v2e  27936  konigsbergiedgw  28026  konigsberglem2  28031  konigsberglem5  28034  s2f1  30621  cycpm2tr  30761  cyc3evpm  30792  indf1o  31283  eulerpartlemgf  31637  sgnpbi  31804  prodfzo03  31874  hgt750lemg  31925  hgt750lemb  31927  tgoldbachgt  31934  sn-1ne2  39156  nn0rppwr  39180  mncn0  39737  aaitgo  39760  fourierdlem60  42450  fourierdlem61  42451  fun2dmnopgexmpl  43482  zlmodzxzel  44402  zlmodzxzscm  44404  zlmodzxzadd  44405  zlmodzxznm  44551  zlmodzxzldeplem  44552  line2  44738  line2x  44740
  Copyright terms: Public domain W3C validator