Theorem 0ne1 10410

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 9372	. 2 |- 1 =/= 0
2	1	necomi 2639	1 |- 0 =/= 1

Syntax hints:   =/= wne 2620   0cc0 9303   1c1 9304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-ext 2423  ax-1ne0 9372

This theorem depends on definitions:  df-bi 185  df-cleq 2436  df-ne 2622

This theorem is referenced by:  s2f1o  12547  f1oun2prg  12548  wrdlen2i  12567  prmreclem2  13999  i1f1lem  21189  mcubic  22264  cubic2  22265  asinlem  22285  sqff1o  22542  dchrpt  22628  lgsqr  22707  usgraexmpl  23341  2trllemH  23473  2trllemE  23474  2wlklemA  23475  2wlklemB  23476  2trllemD  23478  2trllemG  23479  wlkntrllem1  23480  wlkntrllem2  23481  wlkntrllem3  23482  constr1trl  23509  1pthon  23512  2wlklem1  23518  2pthon  23523  constr3lem2  23554  constr3lem4  23555  constr3lem5  23556  constr3trllem1  23558  constr3trllem3  23560  constr3pthlem1  23563  konigsberg  23630  indf1o  26502  sgnpbi  26951  bezoutr1  29355  mncn0  29522  aaitgo  29545  f13idfv  30174  hashrabsn1  30259  usgra2pthspth  30321  usgra2wlkspthlem1  30322  usgra2wlkspthlem2  30323  usgra2pthlem1  30326  zlmodzxzel  30781  zlmodzxzscm  30783  zlmodzxzadd  30784  zlmodzxznm  31036  zlmodzxzldeplem  31037