Theorem 0ne1 10592

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 9550	. 2 |- 1 =/= 0
2	1	necomi 2730	1 |- 0 =/= 1

Syntax hints:   =/= wne 2655   0cc0 9481   1c1 9482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2438  ax-1ne0 9550

This theorem depends on definitions:  df-bi 185  df-cleq 2452  df-ne 2657

This theorem is referenced by:  f13idfv  12062  hashrabsn1  12397  s2f1o  12814  f1oun2prg  12815  wrdlen2i  12834  prmreclem2  14283  i1f1lem  21824  mcubic  22899  cubic2  22900  asinlem  22920  sqff1o  23177  dchrpt  23263  lgsqr  23342  usgraexmpl  24063  2trllemH  24216  2trllemE  24217  2wlklemA  24218  2wlklemB  24219  2trllemD  24221  2trllemG  24222  wlkntrllem1  24223  wlkntrllem2  24224  wlkntrllem3  24225  constr1trl  24252  1pthon  24255  2wlklem1  24261  2pthon  24266  usgra2wlkspthlem1  24281  usgra2wlkspthlem2  24282  constr3lem2  24308  constr3lem4  24309  constr3lem5  24310  constr3trllem1  24312  constr3trllem3  24314  constr3pthlem1  24317  konigsberg  24649  indf1o  27663  sgnpbi  28111  bezoutr1  30515  mncn0  30682  aaitgo  30705  usgra2pthspth  31775  usgra2pthlem1  31777  zlmodzxzel  31883  zlmodzxzscm  31885  zlmodzxzadd  31886  zlmodzxznm  32054  zlmodzxzldeplem  32055