Theorem 0ne1 11278

Description: 0 ≠ 1; 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 10195	. 2 ⊢ 1 ≠ 0
2	1	necomi 2984	1 ⊢ 0 ≠ 1

Syntax hints:   ≠ wne 2930  0cc0 10126  1c1 10127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-ext 2738  ax-1ne0 10195

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1852  df-cleq 2751  df-ne 2931

This theorem is referenced by:  f13idfv  12992  hashrabsn1  13353  prhash2ex  13377  s2f1o  13859  f1oun2prg  13860  wrdlen2i  13885  fprodn0f  14919  mod2eq1n2dvds  15271  bezoutr1  15482  xrsnsgrp  19982  i1f1lem  23653  mcubic  24771  cubic2  24772  asinlem  24792  sqff1o  25105  dchrpt  25189  lgsqr  25273  lgsqrmodndvds  25275  2lgslem4  25328  umgr2v2e  26629  umgr2v2evd2  26631  usgr2trlncl  26864  usgr2pthlem  26867  uspgrn2crct  26909  ntrl2v2e  27308  konigsbergiedgw  27398  konigsberglem2  27403  konigsberglem5  27406  nn0sqeq1  29820  indf1o  30393  eulerpartlemgf  30748  sgnpbi  30915  prodfzo03  30988  hgt750lemg  31039  hgt750lemb  31041  tgoldbachgt  31048  mncn0  38209  aaitgo  38232  fourierdlem60  40884  fourierdlem61  40885  fun2dmnopgexmpl  41809  zlmodzxzel  42641  zlmodzxzscm  42643  zlmodzxzadd  42644  zlmodzxznm  42794  zlmodzxzldeplem  42795