Theorem 0ne1 11700

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

Syntax hints:   ≠ wne 3014  0cc0 10529  1c1 10530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791  ax-1ne0 10598

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-ne 3015

This theorem is referenced by:  f13idfv  13360  hashrabsn1  13727  prhash2ex  13752  s2f1o  14270  f1oun2prg  14271  wrdlen2i  14296  mod2eq1n2dvds  15688  bezoutr1  15905  xrsnsgrp  20573  i1f1lem  24282  mcubic  25417  cubic2  25418  asinlem  25438  sqff1o  25751  dchrpt  25835  lgsqr  25919  lgsqrmodndvds  25921  2lgslem4  25974  umgr2v2e  27299  umgr2v2evd2  27301  usgr2trlncl  27533  usgr2pthlem  27536  uspgrn2crct  27578  ntrl2v2e  27929  konigsbergiedgw  28019  konigsberglem2  28024  konigsberglem5  28027  s2f1  30614  cycpm2tr  30754  cyc3evpm  30785  indf1o  31276  eulerpartlemgf  31630  sgnpbi  31797  prodfzo03  31867  hgt750lemg  31918  hgt750lemb  31920  tgoldbachgt  31927  sn-1ne2  39149  nn0rppwr  39173  mncn0  39730  aaitgo  39753  fourierdlem60  42442  fourierdlem61  42443  fun2dmnopgexmpl  43474  zlmodzxzel  44394  zlmodzxzscm  44396  zlmodzxzadd  44397  zlmodzxznm  44543  zlmodzxzldeplem  44544  line2  44730  line2x  44732