Theorem 0ne1 11032

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 9949	. 2 ⊢ 1 ≠ 0
2	1	necomi 2844	1 ⊢ 0 ≠ 1

Syntax hints:   ≠ wne 2790  0cc0 9880  1c1 9881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601  ax-1ne0 9949

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-ne 2791

This theorem is referenced by:  f13idfv  12740  hashrabsn1  13103  prhash2ex  13127  s2f1o  13597  f1oun2prg  13598  wrdlen2i  13620  fprodn0f  14647  mod2eq1n2dvds  14995  bezoutr1  15206  xrsnsgrp  19701  i1f1lem  23362  mcubic  24474  cubic2  24475  asinlem  24495  sqff1o  24808  dchrpt  24892  lgsqr  24976  lgsqrmodndvds  24978  2lgslem4  25031  uvtxa01vtx  26185  umgr2v2e  26307  umgr2v2evd2  26309  usgr2trlncl  26525  usgr2pthlem  26528  uspgrn2crct  26569  ntrl2v2e  26884  konigsbergiedgw  26974  konigsberglem2  26981  konigsberglem5  26984  nn0sqeq1  29353  indf1o  29864  eulerpartlemgf  30219  sgnpbi  30386  mncn0  37187  aaitgo  37210  fourierdlem60  39687  fourierdlem61  39688  fun2dmnopgexmpl  40597  zlmodzxzel  41418  zlmodzxzscm  41420  zlmodzxzadd  41421  zlmodzxznm  41571  zlmodzxzldeplem  41572