Axiom ax-1ne0 11168

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 11144. (Contributed by NM, 29-Jan-1995.)

Assertion

Ref	Expression
ax-1ne0	⊢ 1 ≠ 0

Detailed syntax breakdown of Axiom ax-1ne0

Step	Hyp	Ref	Expression
1		c1 11100	. 2 class 1
2		cc0 11099	. 2 class 0
3	1, 2	wne 2956	1 wff 1 ≠ 0

This axiom is referenced by:  elimne0  11195  1re  11207  mul02lem2  11386  addrid  11389  ine0  11648  0lt1  11735  recne0  11884  div1  11903  recdiv  11920  divdiv1  11925  divdiv2  11926  recgt0ii  12120  neg1ne0  12204  ind1a  12228  nnne0  12269  0ne1  12311  fvf1tp  13821  expcl2lem  14108  expclzlem  14118  m1expcl2  14120  1exp  14126  hashrabsn1  14409  tpf1ofv1  14533  relexp1g  15062  sgn0bi  15139  geo2sum2  15927  geoihalfsum  15935  fprodntriv  15995  prod0  15996  prod1  15997  fprodn0  16032  fprodn0f  16044  efne0d  16150  efne0OLD  16152  tan0  16206  m1exp1  16433  divalg  16460  gcd1  16585  rpdvds  16717  m1dvdsndvds  16857  pcpre1  16901  pc1  16914  pcrec  16917  pcid  16932  ex-chn2  18693  m1expaddsub  19567  cndrng  21530  cnmgpid  21558  gzrngunitlem  21561  gzrngunit  21562  zringnzr  21589  zringunit  21595  cnmsgnsubg  21706  cnmsgngrp  21708  psgninv  21711  mvrf1  22114  psdmvr  22311  pmatcollpw3fi1lem1  22922  dscmet  24708  xrhmeo  25084  clmopfne  25234  itg11  25829  ply1remlem  26301  dgrid  26400  plyn0mulidp  26421  plyrem  26445  facth  26446  fta1lem  26447  vieta1lem1  26450  vieta1lem2  26451  vieta1  26452  qaa  26463  iaa  26465  coseq00topi  26643  logneg2  26756  logtayl2  26803  1cxp  26813  cxpeq0  26819  logb1  26910  logbmpt  26929  ang180lem4  26953  ang180lem5  26954  isosctrlem2  26960  isosctrlem3  26961  angpined  26971  dcubic2  26985  dcubic  26987  dquartlem1  26992  atandmtan  27061  efrlim  27110  mumullem2  27320  1sgm2ppw  27340  dchrn0  27390  lgsne0  27475  1lgs  27480  gausslemma2dlem0i  27504  lgseisenlem1  27515  lgseisenlem2  27516  lgsquadlem1  27520  lgsquad2lem2  27525  2lgs  27547  2sqlem7  27564  2sqlem8a  27565  2sqlem8  27566  chebbnd2  27617  chto1lb  27618  pnt2  27753  pnt  27754  qabvle  27765  qabvexp  27766  ostthlem2  27768  ostth3  27778  ostth  27779  axlowdimlem6  29263  axlowdimlem13  29270  axlowdimlem14  29271  axlowdim1  29275  usgrexmpldifpr  29574  pthdadjvtx  30043  upgr4cycl4dv4e  30502  konigsberglem1  30569  frgrreggt1  30710  norm1exi  31568  kbpj  32274  largei  32585  indsupp  33153  esplyfvaln  33930  ccfldextdgrr  34028  constrfin  34102  2sqr3minply  34136  cos9thpiminplylem1  34138  cos9thpiminplylem2  34139  cos9thpiminplylem3  34140  cos9thpinconstrlem1  34145  xrge0iif1  34294  cntnevol  34584  ballotlemii  34860  signswch  34914  signstfvcl  34926  indispconn  35680  poimirlem23  38238  25or6to4  42919  tan3rdpi  43059  remulinvcom  43140  sn-rediv1d  43159  rerecne0d  43163  sn-0lt1  43195  0dioph  43457  pell1234qrne0  43528  expgrowth  44993  binomcxplemradcnv  45010  xrralrecnnge  46053  iooiinioc  46220  stoweidlem13  46675  wallispi2lem1  46733  dirkertrigeq  46763  fourierdlem30  46799  fourierdlem62  46830  cjnpoly  47571  dfodd5  48370  usgrexmpl1lem  48731  usgrexmpl2lem  48736  usgrexmpl2nb1  48742  usgrexmpl2trifr  48747  gpgvtxedg0  48773  gpgvtxedg1  48774  gpgedgiov  48775  gpgedg2iv  48777  gpg5nbgrvtx03starlem1  48778  gpg5nbgrvtx03starlem3  48780  gpg5nbgrvtx13starlem1  48781  gpg5nbgrvtx13starlem2  48782  gpg5nbgrvtx13starlem3  48783  gpg3nbgrvtx0  48786  gpg3nbgrvtx0ALT  48787  gpg3nbgrvtx1  48788  gpgprismgr4cycllem2  48806  pgnbgreunbgrlem2lem1  48824  pgnbgreunbgrlem2lem2  48825  pgnbgreunbgrlem2lem3  48826  pgnbgreunbgrlem5lem1  48830  pgnbgreunbgrlem5lem2  48831  pgnbgreunbgrlem5lem3  48832  gpg5edgnedg  48840  itcoval1  49388  line2ylem  49476  sec0  50483