Theorem eqtrd 2210

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtrd	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtrd

Step	Hyp	Ref	Expression
1		eqtrd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eqeq2d 2189	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqtr2d  2211  eqtr3d  2212  eqtr4d  2213  3eqtrd  2214  3eqtrrd  2215  3eqtr2d  2216  eqtrid  2222  eqtrdi  2226  rabeqbidv  2734  rabeqbidva  2735  csbidmg  3115  csbco3g  3117  difeq12d  3256  ifeq12d  3555  ifbieq1d  3558  ifbieq2d  3560  ifbieq12d  3562  eqifdc  3571  csbsng  3655  disjpr2  3658  csbunig  3819  iuneq12d  3912  unisn3  4447  op1stbg  4481  opthreg  4557  onsucuni2  4565  csbxpg  4709  coeq12d  4793  csbdmg  4823  reseq12d  4910  csbresg  4912  resima2  4943  imaeq12d  4973  csbrng  5092  opswapg  5117  relcnvtr  5150  relcoi2  5161  relcoi1  5162  iotaint  5193  funprg  5268  funtpg  5269  funcnvres2  5293  fnco  5326  fococnv2  5489  fveq12d  5524  csbfv12g  5553  csbfv2g  5554  csbfvg  5555  dffn5im  5563  funfvdm2  5582  fvun1  5584  fvmpt2d  5604  fvmptt  5609  fndmin  5625  fniniseg2  5640  fnniniseg2  5641  fmptcof  5685  fvresi  5711  fvunsng  5712  fvpr1g  5724  fvpr2g  5725  fvtp1g  5726  funiunfvdm  5766  fcof1o  5792  riotaeqbidv  5836  oveq123d  5898  csbov12g  5916  csbov1g  5917  csbov2g  5918  ovmpodxf  6002  caov42d  6063  caovdilemd  6068  caovimo  6070  offeq  6098  offval2  6100  caofinvl  6107  ot1stg  6155  ot2ndg  6156  2nd1st  6183  mpomptsx  6200  dmmpossx  6202  fmpox  6203  fmpoco  6219  1stconst  6224  algrflemg  6233  tfrexlem  6337  rdgivallem  6384  rdgisuc1  6387  frec0g  6400  frecabcl  6402  frecsuclem  6409  frecrdg  6411  oa0  6460  oasuc  6467  oa1suc  6470  omsuc  6475  nnaass  6488  nndi  6489  nnmass  6490  nnm2  6529  nn2m  6530  ereq1  6544  errn  6559  uniqs2  6597  oviec  6643  ecovass  6646  ecoviass  6647  ecovdi  6648  ecovidi  6649  mapsnconst  6696  mapen  6848  mapxpen  6850  xpmapenlem  6851  phplem4on  6869  fidifsnen  6872  undifdc  6925  fiintim  6930  fisseneq  6933  snexxph  6951  sbthlemi4  6961  sbthlemi6  6963  supeq2  6990  eqsupti  6997  infvalti  7023  djuf1olem  7054  djuss  7071  1stinl  7075  2ndinl  7076  1stinr  7077  2ndinr  7078  updjudhcoinlf  7081  updjudhcoinrg  7082  omp1eomlem  7095  difinfsn  7101  ctmlemr  7109  ctssdclemn0  7111  ctssdc  7114  enumctlemm  7115  nnnninfeq  7128  nnnninfeq2  7129  nninfisollemne  7131  nninfisol  7133  enwomnilem  7169  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  en2other2  7197  cc3  7269  mulidpi  7319  addasspig  7331  mulasspig  7333  distrpig  7334  indpi  7343  addcmpblnq  7368  mulpipq  7373  dmaddpqlem  7378  nqpi  7379  addcomnqg  7382  recrecnq  7395  ltsonq  7399  ltanqg  7401  ltmnqg  7402  ltaddnq  7408  ltexnqq  7409  archnqq  7418  prarloclemarch  7419  ltrnqg  7421  ltnnnq  7424  nq0nn  7443  addcmpblnq0  7444  nqpnq0nq  7454  nqnq0a  7455  nq0m0r  7457  nq0a0  7458  distrnq0  7460  addassnq0  7463  nq02m  7466  prarloclemlo  7495  prarloclemcalc  7503  addnqprllem  7528  addnqprulem  7529  addnqprl  7530  addnqpru  7531  appdivnq  7564  mulnqprl  7569  mulnqpru  7570  addcanprlemu  7616  ltaprlem  7619  ltmprr  7643  cauappcvgprlemladdrl  7658  mulcmpblnrlemg  7741  mulcomsrg  7758  distrsrg  7760  ltsosr  7765  1idsr  7769  00sr  7770  ltasrg  7771  recexgt0sr  7774  srpospr  7784  prsradd  7787  prsrriota  7789  caucvgsrlemcau  7794  caucvgsrlemgt1  7796  caucvgsrlemoffval  7797  caucvgsrlemoffres  7801  caucvgsr  7803  map2psrprg  7806  elreal2  7831  mulresr  7839  pitonnlem1p1  7847  pitonnlem2  7848  pitoregt0  7850  recidpirqlemcalc  7858  recidpirq  7859  axaddcl  7865  axmulcl  7867  axmulcom  7872  axmulass  7874  axdistr  7875  ax1rid  7878  axcnre  7882  recriota  7891  axcaucvglemcau  7899  mulrid  7956  mullid  7957  adddirp1d  7986  joinlmuladdmuld  7987  muladd11  8092  1p1times  8093  readdcan  8099  comraddd  8116  add42  8121  npcan  8168  addsubass  8169  2addsub  8173  addsubeq4  8174  nppcan  8181  nnpcan  8182  npncan2  8186  nncan  8188  subsub  8189  nnncan  8194  nnncan1  8195  pnpcan2  8199  pnncan  8200  subneg  8208  negneg  8209  negdi2  8217  mvrraddd  8325  assraddsubd  8327  subaddeqd  8328  addid0  8332  mul02  8346  mul01  8348  mulneg1  8354  mul2neg  8357  mulm1  8359  ltadd2  8378  rimul  8544  rereim  8545  mulreim  8563  recextlem1  8610  mulcanapd  8620  divcanap1  8640  divrecap2  8648  divmulassap  8654  divmulasscomap  8655  divcanap4  8658  dividap  8660  muldivdirap  8666  divdivdivap  8672  recdivap  8677  divadddivap  8686  divsubdivap  8687  div2negap  8694  divcanap5rd  8777  dmdcanap2d  8780  subrecap  8798  recgt0  8809  lt2mul2div  8838  nnmulcl  8942  times2  9050  add1p1  9170  sub1m1  9171  cnm2m1cnm3  9172  nn0supp  9230  peano2z  9291  nneoor  9357  supminfex  9599  cnref1o  9652  rexneg  9832  xaddpnf1  9848  xaddmnf1  9850  rexadd  9854  xaddid1  9864  xaddid2  9865  xaddass  9871  xpncan  9873  xleadd1a  9875  xltadd1  9878  xposdif  9884  xadd4d  9887  xleaddadd  9889  iooidg  9911  iooval2  9917  icoshftf1o  9993  lincmb01cmp  10005  iccf1o  10006  fzval2  10013  fzsuc  10071  fzpred  10072  fztpval  10085  fseq1p1m1  10096  fzshftral  10110  fz0to4untppr  10126  fzo0to3tp  10221  fzo0sn0fzo1  10223  fzosplitsn  10235  fzosplitprm1  10236  fzisfzounsn  10238  rebtwn2zlemstep  10255  2tnp1ge0ge0  10303  flqdiv  10323  modqvalr  10327  modqdiffl  10337  modqfrac  10339  modqmulnn  10344  modqid  10351  modqcyc  10361  modqcyc2  10362  mulp1mod1  10367  modqmuladd  10368  modqmuladdnn0  10370  qnegmod  10371  m1modnnsub1  10372  addmodid  10374  addmodidr  10375  modqmul12d  10380  modqnegd  10381  modqadd12d  10382  modifeq2int  10388  modqaddmulmod  10393  modqdi  10394  modqsubdir  10395  modsumfzodifsn  10398  addmodlteq  10400  frec2uzsucd  10403  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdglem  10413  frecuzrdgsuc  10416  frecuzrdgg  10418  frecuzrdgdomlem  10419  frecuzrdgfunlem  10421  frecuzrdgtclt  10423  frecuzrdgsuctlem  10425  frecfzennn  10428  seqeq1  10450  seq3val  10460  seqvalcd  10461  seq3p1  10464  seqp1cd  10468  seq3feq2  10472  seq3fveq  10473  seq3shft2  10475  seq3-1p  10482  iseqf1olemnab  10490  iseqf1olemab  10491  iseqf1olemnanb  10492  iseqf1olemqk  10496  iseqf1olemfvp  10499  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3f1o  10506  seq3id3  10509  seq3z  10513  fser0const  10518  exp3vallem  10523  expnnval  10525  expp1  10529  expn1ap0  10532  mulexp  10561  expaddzaplem  10565  expaddzap  10566  expmul  10567  expp1zap  10571  expm1ap  10572  sqval  10580  sqdividap  10587  iexpcyc  10627  subsq2  10630  qsqeqor  10633  binom2  10634  binom21  10635  binom2sub1  10637  mulbinom2  10639  binom3  10640  zesq  10641  bernneq  10643  sqoddm1div8  10676  mulsubdivbinom2ap  10693  nn0opthlem1d  10702  facp1  10712  faclbnd6  10726  bcval2  10732  bcval3  10733  bcn0  10737  bcp1n  10743  bcp1nk  10744  bcn2  10746  bcp1m1  10747  bcpasc  10748  bcn2m1  10751  hashinfom  10760  hashennn  10762  hashfz1  10765  fseq1hash  10783  omgadd  10784  hashunsng  10789  hashprg  10790  hashdifsn  10801  hashdifpr  10802  hashfz  10803  hashfzo  10804  hashfzo0  10805  hashfzp1  10806  hashfz0  10807  hashxp  10808  resunimafz0  10813  fnfz0hash  10814  ffzo0hash  10816  hashfacen  10818  zfz1isolemsplit  10820  zfz1isolemiso  10821  zfz1isolem1  10822  shftdm  10833  shftval2  10837  shftval4  10839  shftval5  10840  shftcan1  10845  seq3shft  10849  imre  10862  crre  10868  remim  10871  reim0b  10873  recj  10878  reneg  10879  readd  10880  resub  10881  remullem  10882  imcj  10886  imneg  10887  imadd  10888  imsub  10889  cjcj  10894  cjadd  10895  ipcnval  10897  cjneg  10901  cjsub  10903  cjexp  10904  imval2  10905  cjap  10917  resqrexlemf1  11019  resqrexlemfp1  11020  resqrexlemover  11021  resqrexlemcalc1  11025  resqrexlemcalc3  11027  resqrexlemnm  11029  resqrexlemcvg  11030  resqrtcl  11040  sqrtsq  11055  absneg  11061  absvalsq  11064  absvalsq2  11065  sqabsadd  11066  sqabssub  11067  absval2  11068  absreimsq  11078  absmul  11080  absexp  11090  absexpzap  11091  abssuble0  11114  abstri  11115  recan  11120  amgm2  11129  maxabslemlub  11218  max0addsup  11230  minmax  11240  minabs  11246  bdtrilem  11249  bdtri  11250  xrmaxiflemab  11257  xrmaxiflemcom  11259  xrmaxadd  11271  xrminmax  11275  xrmineqinf  11279  xrminrecl  11283  xrbdtri  11286  climshft2  11316  subcn2  11321  reccn2ap  11323  climaddc2  11340  iser3shft  11356  climcvg1nlem  11359  sumeq12dv  11382  sumeq12rdv  11383  sumrbdclem  11387  fsum3cvg  11388  summodclem3  11390  summodclem2a  11391  summodc  11393  fsum3  11397  isumz  11399  fsumf1o  11400  fisumss  11402  fsumsersdc  11405  fsum3ser  11407  fsumsplit  11417  fsumsplitf  11418  sumsnf  11419  fsumsplitsn  11420  fsum1  11422  sumpr  11423  sumtp  11424  fsumm1  11426  fsum1p  11428  fsumsplitsnun  11429  fsump1  11430  isumclim  11431  sumnul  11434  isumadd  11441  fsum2dlemstep  11444  fsumcnv  11447  fisumcom2  11448  fsumshftm  11455  fisumrev2  11456  fisum0diag2  11457  fsumsub  11462  fsumdifsnconst  11465  modfsummodlemstep  11467  fsumabs  11475  telfsumo  11476  telfsum  11478  telfsum2  11479  fsumparts  11480  fsumiun  11487  hashiun  11488  hash2iun  11489  hash2iun1dif1  11490  binomlem  11493  binom1p  11495  binom11  11496  binom1dif  11497  bcxmas  11499  isum1p  11502  isumnn0nn  11503  isumlessdc  11506  divcnv  11507  arisum2  11509  trireciplem  11510  geosergap  11516  geolim  11521  georeclim  11523  geo2lim  11526  geoisum1  11529  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratnnlemsumlt  11538  cvgratz  11542  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodfrecap  11556  prodeq12dv  11579  prodeq12rdv  11580  prodrbdclem  11581  fproddccvg  11582  prodmodclem3  11585  prodmodclem2a  11586  zprodap0  11591  fprodseq  11593  fprodntrivap  11594  prod1dc  11596  fprodf1o  11598  prodssdc  11599  fprodssdc  11600  prodsnf  11602  fprod1  11604  fprodsplitdc  11606  fprodm1  11608  fprod1p  11609  fprodp1  11610  fprodunsn  11614  fprodcl2lem  11615  fprodabs  11626  fprodconst  11630  fprod2dlemstep  11632  fprodcnv  11635  fprodcom2fi  11636  fprodrec  11639  fprodsplitsn  11643  fprodsplit1f  11644  fprodeq0g  11648  eftabs  11666  efcllemp  11668  ef0lem  11670  efcvgfsum  11677  ege2le3  11681  efcj  11683  efaddlem  11684  efexp  11692  eftlub  11700  efsep  11701  effsumlt  11702  ef4p  11704  efgt1p2  11705  efgt1p  11706  tanval2ap  11723  tanval3ap  11724  resinval  11725  recosval  11726  efi4p  11727  resin4p  11728  recos4p  11729  sinneg  11736  cosneg  11737  tannegap  11738  efmival  11743  sinadd  11746  cosadd  11747  tanaddaplem  11748  tanaddap  11749  sinsub  11750  cossub  11751  addsin  11752  subsin  11753  subcos  11757  sincossq  11758  sin2t  11759  sin01bnd  11767  cos01bnd  11768  absefi  11778  absef  11779  absefib  11780  efieq1re  11781  demoivre  11782  demoivreALT  11783  eirraplem  11786  dvdstr  11837  dvdsadd2b  11849  mulmoddvds  11871  ltoddhalfle  11900  opoe  11902  m1expo  11907  m1exp1  11908  flodddiv4  11941  flodddiv4t2lthalf  11944  zsupcllemstep  11948  nn0gcdid0  11984  gcdaddm  11987  gcdadd  11988  gcdid  11989  gcdabs  11991  modgcd  11994  1gcd  11995  bezout  12014  dfgcd2  12017  mulgcd  12019  absmulgcd  12020  gcdmultiple  12023  gcdmultiplez  12024  rpmulgcd  12029  rplpwr  12030  rppwr  12031  dvdssqlem  12033  uzwodc  12040  ialgr0  12046  alginv  12049  algcvg  12050  algfx  12054  eucalginv  12058  eucalglt  12059  lcmcl  12074  lcmabs  12078  lcmgcdlem  12079  lcmdvds  12081  lcmgcdnn  12084  coprmdvds  12094  qredeq  12098  divgcdcoprm0  12103  divgcdcoprmex  12104  rpexp1i  12156  sqrt2irrlem  12163  sqpweven  12177  2sqpwodd  12178  sqrt2irraplemnn  12181  qmuldeneqnum  12197  nn0gcdsq  12202  numdensq  12204  nn0sqrtelqelz  12208  phibndlem  12218  dfphi2  12222  phiprmpw  12224  phiprm  12225  phimullem  12227  eulerthlem1  12229  eulerthlemh  12233  eulerthlemth  12234  eulerth  12235  prmdiv  12237  hashgcdlem  12240  phisum  12242  odzdvds  12247  vfermltl  12253  powm2modprm  12254  modprm0  12256  nnnn0modprm0  12257  coprimeprodsq  12259  pythagtriplem1  12267  pythagtriplem3  12269  pythagtriplem4  12270  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem14  12279  pythagtriplem16  12281  pceulem  12296  pcval  12298  pczpre  12299  pcdiv  12304  pc1  12307  pcrec  12310  pcexp  12311  pcid  12325  pcneg  12326  pcgcd1  12329  pc2dvds  12331  difsqpwdvds  12339  pcaddlem  12340  pcadd  12341  pcmpt  12343  pcmpt2  12344  pcprod  12346  pcfac  12350  prmpwdvds  12355  pockthlem  12356  1arithlem2  12364  4sqlem9  12386  4sqlem4  12392  mul4sqlem  12393  ennnfonelemp1  12409  ennnfonelemhdmp1  12412  ennnfonelemss  12413  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemhom  12418  ennnfonelemnn0  12425  ctinfomlemom  12430  setsvala  12495  fvsetsid  12498  setsresg  12502  setscom  12504  setsslid  12515  ressbasd  12529  ressabsg  12537  restid2  12702  prdsex  12723  imasex  12731  imasival  12732  qusval  12749  xpsff1o  12773  lidrididd  12806  grprinvd  12810  mndpropd  12846  mhmf1o  12866  mhmco  12879  grpinvval  12921  isgrpinv  12931  grpsubinv  12948  grpidssd  12951  grpinvsub  12957  grpsubid  12959  grpsubadd0sub  12962  grpsubsub  12964  grpnpncan0  12971  grpnnncan2  12972  grpsubpropd2  12980  grp1inv  12982  ghmgrp  12987  mulgnn  12994  mulgnnp1  12996  mulg2  12997  mulgnegnn  12998  mulgneg  13006  mulgnegneg  13007  mulgm1  13008  mulgaddcom  13012  mulginvcom  13013  mulgnn0z  13015  mulgz  13016  mulgnn0dir  13018  mulgdirlem  13019  mulgp1  13021  mulgnnass  13023  mulgnn0ass  13024  mulgass  13025  mulgassr  13026  mhmmulg  13029  mulgpropdg  13030  subg0  13045  subgmulg  13053  issubg4m  13058  isnsg3  13072  nmzsubg  13075  0nsg  13079  eqger  13088  eqgid  13090  eqgcpbl  13092  rinvmod  13117  ablsub4  13121  ablpncan3  13125  ablnnncan  13131  ablnnncan1  13132  mgptopng  13144  srgass  13159  srgmulgass  13177  srgpcomp  13178  srgpcomppsc  13180  srglmhm  13181  srgrmhm  13182  ringcom  13219  ringpropd  13222  crngpropd  13223  isringd  13225  iscrngd  13226  ringinvnzdiv  13232  ringnegl  13233  ringnegr  13234  ringsubdi  13238  ringsubdir  13239  mulgass2  13240  opprmulg  13248  opprring  13254  oppr1g  13257  isunitd  13280  unitmulcl  13287  unitgrp  13290  invrfvald  13296  dvrid  13311  dvrcan1  13314  rdivmuldivd  13318  rngidpropdg  13320  unitpropdg  13322  invrpropdg  13323  subrguss  13362  subrgdv  13364  subrgunit  13365  subrgpropd  13374  aprval  13377  islmod  13386  islmodd  13388  lmodvs0  13417  lmodvsmmulgdi  13418  lmodfopne  13421  lmodcom  13428  lmodnegadd  13431  lmodsubvs  13438  lmodsubdir  13440  lmodprop2d  13443  rmodislmodlem  13445  rmodislmod  13446  lsssetm  13449  islssmd  13451  lssuni  13455  lsssn0  13461  cncrng  13502  zsssubrg  13518  ntrval  13649  clsval  13650  cldcls  13653  neival  13682  resttop  13709  restco  13713  restabs  13714  resttopon2  13717  cnpval  13737  cnntr  13764  cnrest2  13775  upxp  13811  uptx  13813  cnmpt11  13822  cnmpt21  13830  psmetsym  13868  psmetres2  13872  xmetsym  13907  xmettxlem  14048  txmetcnp  14057  cnbl0  14073  cnblcld  14074  remetdval  14078  bl2ioo  14081  tgioo  14085  addcncntoplem  14090  divcnap  14094  fsumcncntop  14095  cncfmet  14118  cncfmptc  14121  addccncf  14125  negcncf  14127  mulcncflem  14129  ivthinclemlopn  14153  limcimolemlt  14172  cnplimcim  14175  cnplimclemr  14177  limccnp2lem  14184  limccnp2cntop  14185  dvfvalap  14189  dvconst  14200  dvaddxxbr  14204  dvmulxxbr  14205  dvcjbr  14211  dvexp  14214  dvrecap  14216  dvmptclx  14219  dvmptaddx  14220  dvmptmulx  14221  dvmptcmulcn  14222  dveflem  14226  dvef  14227  reeff1oleme  14232  sin0pilem1  14241  sin0pilem2  14242  efper  14267  sinperlem  14268  sinmpi  14275  cosmpi  14276  sinppi  14277  cosppi  14278  efimpi  14279  ptolemy  14284  sinq12gt0  14290  coseq0negpitopi  14296  tangtx  14298  abssinper  14306  cosq34lt1  14310  relogexp  14332  logdivlti  14341  logcxp  14357  rpcxp0  14358  rpcxp1  14359  1cxp  14360  ecxp  14361  rpcxpadd  14365  rpcxpp1  14366  rpmulcxp  14369  rpdivcxp  14371  cxpmul  14372  rpcxproot  14373  abscxp  14374  rpcxpsqrtth  14389  rplogbid1  14404  rplogb1  14405  rpelogb  14406  rplogbreexp  14410  rplogbzexp  14411  rprelogbmul  14412  rprelogbmulexp  14413  rprelogbdiv  14414  logbrec  14417  rpcxplogb  14421  logbgcd1irr  14424  logbgcd1irraplemexp  14425  logbgcd1irraplemap  14426  binom4  14436  lgslem1  14440  lgsval2lem  14450  lgsvalmod  14459  lgsneg  14464  lgsdir2lem4  14471  lgsdirprm  14474  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgsmodeq  14485  lgsdirnn0  14487  lgsdinn0  14488  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  2lgsoddprmlem1  14492  2lgsoddprmlem2  14493  2sqlem3  14503  2sqlem4  14504  2sqlem8  14509  djucllem  14591  bj-charfun  14598  bj-charfundc  14599  bj-charfundcALT  14600  nninfsellemeq  14802  nninffeq  14808  qdencn  14814  cvgcmp2nlemabs  14819  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  apdifflemf  14833  redcwlpolemeq1  14841  dceqnconst  14846  dcapnconst  14847  nconstwlpolem0  14849  nconstwlpolemgt0  14850  nconstwlpolem  14851