Theorem 0ne1 10644

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 9591	. 2 |- 1 =/= 0
2	1	necomi 2673	1 |- 0 =/= 1

Syntax hints:   =/= wne 2598   0cc0 9522   1c1 9523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380  ax-1ne0 9591

This theorem depends on definitions:  df-bi 185  df-cleq 2394  df-ne 2600

This theorem is referenced by:  f13idfv  12150  hashrabsn1  12490  prhash2ex  12513  s2f1o  12920  f1oun2prg  12921  wrdlen2i  12940  prmreclem2  14644  xrsnsgrp  18774  i1f1lem  22388  mcubic  23503  cubic2  23504  asinlem  23524  sqff1o  23837  dchrpt  23923  lgsqr  24002  usgraexmpl  24818  2trllemH  24971  2trllemE  24972  2wlklemA  24973  2wlklemB  24974  2trllemD  24976  2trllemG  24977  wlkntrllem1  24978  wlkntrllem2  24979  wlkntrllem3  24980  constr1trl  25007  1pthon  25010  2wlklem1  25016  2pthon  25021  usgra2wlkspthlem1  25036  usgra2wlkspthlem2  25037  constr3lem2  25063  constr3lem4  25064  constr3lem5  25065  constr3trllem1  25067  constr3trllem3  25069  constr3pthlem1  25072  konigsberg  25404  nn0sqeq1  28009  indf1o  28471  eulerpartlemgf  28824  sgnpbi  28991  bezoutr1  35285  mncn0  35452  aaitgo  35475  fprodn0f  36962  fourierdlem60  37317  fourierdlem61  37318  mod2eq1n2dvds  37676  usgra2pthspth  37980  usgra2pthlem1  37982  zlmodzxzel  38455  zlmodzxzscm  38457  zlmodzxzadd  38458  zlmodzxznm  38609  zlmodzxzldeplem  38610