Theorem 0ne1 12196

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

Syntax hints:   ≠ wne 2928  0cc0 11006  1c1 11007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703  ax-1ne0 11075

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  f13idfv  13907  hashrabsn1  14281  prhash2ex  14306  s2f1o  14823  f1oun2prg  14824  wrdlen2i  14849  mod2eq1n2dvds  16258  nn0rppwr  16472  bezoutr1  16480  xrsnsgrp  21344  i1f1lem  25617  mcubic  26784  cubic2  26785  asinlem  26805  sqff1o  27119  dchrpt  27205  lgsqr  27289  lgsqrmodndvds  27291  2lgslem4  27344  umgr2v2e  29504  umgr2v2evd2  29506  usgr2trlncl  29738  usgr2pthlem  29741  uspgrn2crct  29786  ntrl2v2e  30138  konigsbergiedgw  30228  konigsberglem2  30233  konigsberglem5  30236  sgnpbi  32822  indf1o  32845  indfsid  32850  s2f1  32926  cycpm2tr  33088  cyc3evpm  33119  evl1deg1  33539  evl1deg2  33540  evl1deg3  33541  rtelextdg2lem  33739  eulerpartlemgf  34392  prodfzo03  34616  hgt750lemg  34667  hgt750lemb  34669  tgoldbachgt  34676  lcmineqlem11  42142  sn-1ne2  42368  expeq1d  42427  sn-nnne0  42563  sn-inelr  42590  mncn0  43242  aaitgo  43265  fourierdlem60  46274  fourierdlem61  46275  fun2dmnopgexmpl  47394  usgrexmpl1lem  48131  usgrexmpl2lem  48136  usgrexmpl2nb0  48141  gpgusgralem  48166  gpgedg2ov  48176  gpg5nbgrvtx03starlem1  48178  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx03starlem3  48180  gpg5nbgrvtx13starlem1  48181  gpg5nbgrvtx13starlem3  48183  gpg3nbgrvtx0  48186  gpg3nbgrvtx0ALT  48187  gpg3nbgrvtx1  48188  gpgprismgr4cycllem2  48206  gpgprismgr4cycllem7  48211  pgnioedg1  48218  pgnioedg2  48219  pgnioedg3  48220  pgnioedg4  48221  pgnioedg5  48222  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  zlmodzxzel  48465  zlmodzxzscm  48467  zlmodzxzadd  48468  zlmodzxznm  48608  zlmodzxzldeplem  48609  fv2arycl  48759  2arymptfv  48761  2arymaptf1  48764  2arymaptfo  48765  line2  48863  line2x  48865