Theorem 0ne1 10965

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 9884	. 2 ⊢ 1 ≠ 0
2	1	necomi 2836	1 ⊢ 0 ≠ 1

Syntax hints:   ≠ wne 2780  0cc0 9815  1c1 9816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590  ax-1ne0 9884

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  f13idfv  12662  hashrabsn1  13024  prhash2ex  13048  s2f1o  13511  f1oun2prg  13512  wrdlen2i  13534  fprodn0f  14561  mod2eq1n2dvds  14909  bezoutr1  15120  xrsnsgrp  19601  i1f1lem  23262  mcubic  24374  cubic2  24375  asinlem  24395  sqff1o  24708  dchrpt  24792  lgsqr  24876  lgsqrmodndvds  24878  2lgslem4  24931  2trllemH  26082  2trllemE  26083  2wlklemA  26084  2wlklemB  26085  2trllemD  26087  2trllemG  26088  wlkntrllem1  26089  wlkntrllem2  26090  wlkntrllem3  26091  constr1trl  26118  1pthon  26121  2wlklem1  26127  2pthon  26132  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  constr3lem2  26174  constr3lem4  26175  constr3lem5  26176  constr3trllem1  26178  constr3trllem3  26180  constr3pthlem1  26183  konigsberg  26514  nn0sqeq1  28901  indf1o  29413  eulerpartlemgf  29768  sgnpbi  29935  mncn0  36728  aaitgo  36751  fourierdlem60  39059  fourierdlem61  39060  fun2dmnopgexmpl  40329  uvtxa01vtx  40624  umgr2v2e  40741  umgr2v2evd2  40743  usgr2trlncl  40966  usgr2pthlem  40969  uspgrn2crct  41011  ntrl2v2e  41325  konigsbergiedgw  41416  konigsberglem2  41423  konigsberglem5  41426  zlmodzxzel  41926  zlmodzxzscm  41928  zlmodzxzadd  41929  zlmodzxznm  42080  zlmodzxzldeplem  42081