Theorem 0ne1 11446

Description: Zero is different from one (the commuted form is the axiom ax-1ne0 10341). (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 10341	. 2 ⊢ 1 ≠ 0
2	1	necomi 3022	1 ⊢ 0 ≠ 1

Syntax hints:   ≠ wne 2968  0cc0 10272  1c1 10273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753  ax-1ne0 10341

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2769  df-ne 2969

This theorem is referenced by:  f13idfv  13118  hashrabsn1  13478  prhash2ex  13501  s2f1o  14067  f1oun2prg  14068  wrdlen2i  14093  mod2eq1n2dvds  15475  bezoutr1  15688  xrsnsgrp  20178  i1f1lem  23893  mcubic  25025  cubic2  25026  asinlem  25046  sqff1o  25360  dchrpt  25444  lgsqr  25528  lgsqrmodndvds  25530  2lgslem4  25583  umgr2v2e  26873  umgr2v2evd2  26875  usgr2trlncl  27112  usgr2pthlem  27115  uspgrn2crct  27157  ntrl2v2e  27561  konigsbergiedgw  27654  konigsberglem2  27659  konigsberglem5  27662  nn0sqeq1  30078  indf1o  30684  eulerpartlemgf  31039  sgnpbi  31207  prodfzo03  31283  hgt750lemg  31334  hgt750lemb  31336  tgoldbachgt  31343  nn0rppwr  38144  mncn0  38650  aaitgo  38673  fourierdlem60  41292  fourierdlem61  41293  fun2dmnopgexmpl  42307  zlmodzxzel  43130  zlmodzxzscm  43132  zlmodzxzadd  43133  zlmodzxznm  43283  zlmodzxzldeplem  43284  line2  43470  line2x  43472