Theorem 0ne1 10699

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 9626	. 2 |- 1 =/= 0
2	1	necomi 2697	1 |- 0 =/= 1

Syntax hints:   =/= wne 2641   0cc0 9557   1c1 9558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451  ax-1ne0 9626

This theorem depends on definitions:  df-bi 190  df-cleq 2464  df-ne 2643

This theorem is referenced by:  f13idfv  12250  hashrabsn1  12591  prhash2ex  12614  s2f1o  13070  f1oun2prg  13071  wrdlen2i  13093  fprodn0f  14122  prmreclem2  14940  xrsnsgrp  19081  i1f1lem  22726  mcubic  23852  cubic2  23853  asinlem  23873  sqff1o  24188  dchrpt  24274  lgsqr  24353  2trllemH  25361  2trllemE  25362  2wlklemA  25363  2wlklemB  25364  2trllemD  25366  2trllemG  25367  wlkntrllem1  25368  wlkntrllem2  25369  wlkntrllem3  25370  constr1trl  25397  1pthon  25400  2wlklem1  25406  2pthon  25411  usgra2wlkspthlem1  25426  usgra2wlkspthlem2  25427  constr3lem2  25453  constr3lem4  25454  constr3lem5  25455  constr3trllem1  25457  constr3trllem3  25459  constr3pthlem1  25462  konigsberg  25794  nn0sqeq1  28399  indf1o  28919  eulerpartlemgf  29285  sgnpbi  29490  bezoutr1  35907  mncn0  36069  aaitgo  36099  fourierdlem60  38142  fourierdlem61  38143  mod2eq1n2dvds  38870  fun2dmnopgexmpl  39174  uvtxa01vtx  39634  umgr2v2e  39748  umgr2v2evd2  39750  uspgrn2crct  39986  ntrl2v2e  40046  konigsbergiedgw  40160  konigsberglem2  40167  konigsberglem5  40170  usgra2pthspth  40173  usgra2pthlem1  40175  zlmodzxzel  40644  zlmodzxzscm  40646  zlmodzxzadd  40647  zlmodzxznm  40798  zlmodzxzldeplem  40799