Theorem 0ne1 12264

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

Syntax hints:   ≠ wne 2926  0cc0 11075  1c1 11076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702  ax-1ne0 11144

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  f13idfv  13972  hashrabsn1  14346  prhash2ex  14371  s2f1o  14889  f1oun2prg  14890  wrdlen2i  14915  mod2eq1n2dvds  16324  nn0rppwr  16538  bezoutr1  16546  xrsnsgrp  21326  i1f1lem  25597  mcubic  26764  cubic2  26765  asinlem  26785  sqff1o  27099  dchrpt  27185  lgsqr  27269  lgsqrmodndvds  27271  2lgslem4  27324  umgr2v2e  29460  umgr2v2evd2  29462  usgr2trlncl  29697  usgr2pthlem  29700  uspgrn2crct  29745  ntrl2v2e  30094  konigsbergiedgw  30184  konigsberglem2  30189  konigsberglem5  30192  sgnpbi  32771  indf1o  32794  s2f1  32873  cycpm2tr  33083  cyc3evpm  33114  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  rtelextdg2lem  33723  eulerpartlemgf  34377  prodfzo03  34601  hgt750lemg  34652  hgt750lemb  34654  tgoldbachgt  34661  lcmineqlem11  42034  sn-1ne2  42260  expeq1d  42319  sn-nnne0  42455  sn-inelr  42482  mncn0  43135  aaitgo  43158  fourierdlem60  46171  fourierdlem61  46172  fun2dmnopgexmpl  47289  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  gpgusgralem  48051  gpgedg2ov  48061  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  gpg3nbgrvtx0  48071  gpg3nbgrvtx0ALT  48072  gpg3nbgrvtx1  48073  gpgprismgr4cycllem2  48090  gpgprismgr4cycllem7  48095  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  zlmodzxzel  48347  zlmodzxzscm  48349  zlmodzxzadd  48350  zlmodzxznm  48490  zlmodzxzldeplem  48491  fv2arycl  48641  2arymptfv  48643  2arymaptf1  48646  2arymaptfo  48647  line2  48745  line2x  48747