Theorem 0ne1 11696

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

Syntax hints:   ≠ wne 2987  0cc0 10526  1c1 10527

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770  ax-1ne0 10595

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  f13idfv  13363  hashrabsn1  13731  prhash2ex  13756  s2f1o  14269  f1oun2prg  14270  wrdlen2i  14295  mod2eq1n2dvds  15688  bezoutr1  15903  xrsnsgrp  20127  i1f1lem  24293  mcubic  25433  cubic2  25434  asinlem  25454  sqff1o  25767  dchrpt  25851  lgsqr  25935  lgsqrmodndvds  25937  2lgslem4  25990  umgr2v2e  27315  umgr2v2evd2  27317  usgr2trlncl  27549  usgr2pthlem  27552  uspgrn2crct  27594  ntrl2v2e  27943  konigsbergiedgw  28033  konigsberglem2  28038  konigsberglem5  28041  s2f1  30647  cycpm2tr  30811  cyc3evpm  30842  indf1o  31393  eulerpartlemgf  31747  sgnpbi  31914  prodfzo03  31984  hgt750lemg  32035  hgt750lemb  32037  tgoldbachgt  32044  lcmineqlem11  39327  sn-1ne2  39466  nn0rppwr  39490  sn-inelr  39590  mncn0  40083  aaitgo  40106  fourierdlem60  42808  fourierdlem61  42809  fun2dmnopgexmpl  43840  zlmodzxzel  44757  zlmodzxzscm  44759  zlmodzxzadd  44760  zlmodzxznm  44906  zlmodzxzldeplem  44907  fv2arycl  45062  2arymptfv  45064  2arymaptf1  45067  2arymaptfo  45068  line2  45166  line2x  45168