Theorem 0ne1 11709

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

Syntax hints:   ≠ wne 3016  0cc0 10537  1c1 10538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793  ax-1ne0 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-ne 3017

This theorem is referenced by:  f13idfv  13369  hashrabsn1  13736  prhash2ex  13761  s2f1o  14278  f1oun2prg  14279  wrdlen2i  14304  mod2eq1n2dvds  15696  bezoutr1  15913  xrsnsgrp  20581  i1f1lem  24290  mcubic  25425  cubic2  25426  asinlem  25446  sqff1o  25759  dchrpt  25843  lgsqr  25927  lgsqrmodndvds  25929  2lgslem4  25982  umgr2v2e  27307  umgr2v2evd2  27309  usgr2trlncl  27541  usgr2pthlem  27544  uspgrn2crct  27586  ntrl2v2e  27937  konigsbergiedgw  28027  konigsberglem2  28032  konigsberglem5  28035  s2f1  30621  cycpm2tr  30761  cyc3evpm  30792  indf1o  31283  eulerpartlemgf  31637  sgnpbi  31804  prodfzo03  31874  hgt750lemg  31925  hgt750lemb  31927  tgoldbachgt  31934  sn-1ne2  39178  nn0rppwr  39202  mncn0  39759  aaitgo  39782  fourierdlem60  42471  fourierdlem61  42472  fun2dmnopgexmpl  43503  zlmodzxzel  44423  zlmodzxzscm  44425  zlmodzxzadd  44426  zlmodzxznm  44572  zlmodzxzldeplem  44573  line2  44759  line2x  44761