Theorem 0ne1 11088

Description: 0 ≠ 1 (common case); the reverse order is already proved. (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 10005	. 2 ⊢ 1 ≠ 0
2	1	necomi 2848	1 ⊢ 0 ≠ 1

Syntax hints:   ≠ wne 2794  0cc0 9936  1c1 9937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602  ax-1ne0 10005

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  f13idfv  12800  hashrabsn1  13163  prhash2ex  13187  s2f1o  13661  f1oun2prg  13662  wrdlen2i  13686  fprodn0f  14722  mod2eq1n2dvds  15071  bezoutr1  15282  xrsnsgrp  19782  i1f1lem  23456  mcubic  24574  cubic2  24575  asinlem  24595  sqff1o  24908  dchrpt  24992  lgsqr  25076  lgsqrmodndvds  25078  2lgslem4  25131  uvtxa01vtx  26298  umgr2v2e  26421  umgr2v2evd2  26423  usgr2trlncl  26656  usgr2pthlem  26659  uspgrn2crct  26700  ntrl2v2e  27018  konigsbergiedgw  27108  konigsberglem2  27115  konigsberglem5  27118  nn0sqeq1  29513  indf1o  30086  eulerpartlemgf  30441  sgnpbi  30608  prodfzo03  30681  hgt750lemg  30732  hgt750lemb  30734  tgoldbachgt  30741  mncn0  37709  aaitgo  37732  fourierdlem60  40383  fourierdlem61  40384  fun2dmnopgexmpl  41303  zlmodzxzel  42133  zlmodzxzscm  42135  zlmodzxzadd  42136  zlmodzxznm  42286  zlmodzxzldeplem  42287