Theorem 0ne1 11301

Description: 0 ≠ 1; 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 10218	. 2 ⊢ 1 ≠ 0
2	1	necomi 2987	1 ⊢ 0 ≠ 1

Syntax hints:   ≠ wne 2933  0cc0 10149  1c1 10150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-ext 2741  ax-1ne0 10218

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2754  df-ne 2934

This theorem is referenced by:  f13idfv  13015  hashrabsn1  13376  prhash2ex  13400  s2f1o  13882  f1oun2prg  13883  wrdlen2i  13908  fprodn0f  14942  mod2eq1n2dvds  15294  bezoutr1  15505  xrsnsgrp  20005  i1f1lem  23676  mcubic  24795  cubic2  24796  asinlem  24816  sqff1o  25129  dchrpt  25213  lgsqr  25297  lgsqrmodndvds  25299  2lgslem4  25352  umgr2v2e  26653  umgr2v2evd2  26655  usgr2trlncl  26888  usgr2pthlem  26891  uspgrn2crct  26933  ntrl2v2e  27332  konigsbergiedgw  27422  konigsberglem2  27427  konigsberglem5  27430  nn0sqeq1  29844  indf1o  30417  eulerpartlemgf  30772  sgnpbi  30939  prodfzo03  31012  hgt750lemg  31063  hgt750lemb  31065  tgoldbachgt  31072  mncn0  38230  aaitgo  38253  fourierdlem60  40905  fourierdlem61  40906  fun2dmnopgexmpl  41830  zlmodzxzel  42662  zlmodzxzscm  42664  zlmodzxzadd  42665  zlmodzxznm  42815  zlmodzxzldeplem  42816