MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3d Structured version   Unicode version

Theorem 3eqtr3d 2465
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3d.1  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3d  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
31, 2eqtr3d 2459 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2459 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-cleq 2416
This theorem is referenced by:  mpteqb  5919  fvmptt  5920  fsnunfv  6058  f1ocnvfv1  6129  f1ocnvfv2  6130  fcof1  6139  weniso  6199  caov12d  6443  caov13d  6445  caov411d  6447  caovmo  6459  grprinvlem  6460  grprinvd  6461  grpridd  6462  onovuni  7011  tfrlem5  7048  seqomlem1  7117  seqomlem4  7120  onasuc  7180  onesuc  7182  oeeui  7253  fopwdom  7628  unxpdomlem2  7725  cantnfres  8129  cnfcom2lem  8153  cnfcom2  8154  cardiun  8363  ackbij1lem16  8611  ackbij2lem2  8616  fpwwe2lem6  9006  fpwwe2lem8  9008  canthp1lem2  9024  mul12  9745  mul4  9748  addid1  9759  addcan  9763  addcom  9765  addcomd  9781  add12  9792  ppncan  9862  addsub4  9863  muladd  9997  mulcand  10191  receu  10203  div13  10237  divdivdiv  10254  divcan5  10255  divdiv1  10264  divdiv2  10265  halfaddsub  10792  xadddi  11527  xov1plusxeqvd  11724  fztp  11798  flzadd  12004  fldiv  12032  modnegd  12090  modsub12d  12092  2submod  12096  seqm1  12175  seqcaopr  12195  seqf1o  12199  exprec  12258  expsub  12265  zesq  12340  digit1  12351  discr1  12353  discr  12354  facnn2  12413  faclbnd6  12429  hashfz1  12474  hashdom  12503  hashun  12506  hashbclem  12558  hashfac  12564  seqcoll  12570  ccatopth  12767  repsw2  12964  repsw3  12965  shftval3  13078  crre  13116  resub  13129  imsub  13137  cjsub  13151  abslem2  13341  sqreulem  13361  climshft2  13584  isercolllem2  13667  iseraltlem2  13687  iseraltlem3  13688  fsumsub  13787  telfsumo  13800  telfsumo2  13801  hashiun  13820  bcxmas  13831  climcndslem1  13845  climcndslem2  13846  trireciplem  13858  geoser  13863  geo2sum2  13868  fprodm1  13959  fallfacfwd  14027  binomfallfaclem2  14031  bpolydiflem  14045  bpoly4  14050  fsumcube  14051  sinsub  14160  cossub  14161  rpnnen2lem10  14214  ruclem12  14231  divalglem9  14319  divalglem9OLD  14320  bitsinv1lem  14353  bitsinv1  14354  bitsf1  14358  sadasslem  14382  bitsres  14385  smup1  14401  smumul  14405  modgcd  14438  absmulgcd  14453  gcdmultiplez  14457  eucalg  14484  lcmgcd  14510  lcmid  14512  lcmftp  14547  numdensq  14641  dfphi2  14660  phiprm  14663  fermltl  14670  prmdiveq  14672  odzdvds  14678  odzdvdsOLD  14684  powm2modprm  14692  modprm0  14694  coprimeprodsq  14697  pythagtriplem6  14709  pythagtriplem7  14710  pythagtriplem12  14714  pythagtriplem16  14718  pcaddlem  14771  sumhash  14779  pcfac  14782  pockthlem  14787  prmreclem6  14803  4sqlem12  14838  4sqlem15OLD  14841  4sqlem15  14847  vdwlem3  14871  vdwlem6  14874  vdwlem9  14877  ramub1lem2  14923  cshwshashlem2  15005  qusaddvallem  15395  xpsaddlem  15419  xpsvsca  15423  mrcun  15466  homfeqval  15540  comfeqval  15551  sectcan  15598  sectco  15599  sectmon  15625  monsect  15626  funcsect  15715  setcmon  15920  resscatc  15938  catciso  15940  evlfcllem  16044  curf2cl  16054  curfcl  16055  yonedalem4c  16100  yonedalem3b  16102  yonedainv  16104  latj12  16280  mnd12g  16490  resmhm  16544  pwsco2mhm  16556  frmdup3lem  16588  grprcan  16637  grplcan  16656  grpinv11  16661  grpinvnz  16663  grplmulf1o  16666  grpinvpropd  16667  grpinvadd  16670  grpsubsub4  16685  mulgz  16717  mulgdirlem  16720  mulgdir  16721  mulgass  16726  mulgsubdir  16727  mulgpropd  16729  pwsmulg  16738  imasgrp2  16739  mhmid  16745  mhmmnd  16746  isnsg3  16789  nmzsubg  16796  ssnmz  16797  eqger  16805  eqglact  16806  ghminv  16828  conjnmz  16854  subgga  16892  gasubg  16894  galcan  16896  gacan  16897  cntzsubg  16928  cntzmhm  16930  psgnunilem2  17074  sylow1lem1  17188  sylow2blem2  17211  sylow2blem3  17212  lsmmod  17263  lsmpropd  17265  lsmdisj2  17270  subgdisj1  17279  subgdisj2  17280  efgredleme  17331  efgredlemd  17332  efgredlemc  17333  efgredlem  17335  frgpup3lem  17365  mulgdi  17405  ghmcmn  17410  lsm4  17436  cygabl  17463  gsummhm2  17510  gsumpt  17532  gsum2d  17542  dprdfeq0  17593  ablfac1eu  17644  ringcom  17747  isringd  17753  ringlz  17755  ringrz  17756  ring1eq0  17758  ringmneg1  17762  gsumdixp  17775  unitgrp  17833  irredrmul  17873  drngmul0or  17934  subrginv  17962  subrgunit  17964  abvrec  18002  srngnvl  18022  srngadd  18023  srngmul  18024  issrngd  18027  lmodvs0  18063  lmodvneg1  18069  lmodcom  18072  lmodsubdi  18083  lmodvsinv  18197  lmodvsinv2  18198  lmhmvsca  18206  lvecvs0or  18269  lvecinv  18274  lspsnvs  18275  lspabs2  18281  lspfixed  18289  lspsolv  18304  unitrrg  18455  asclpropd  18508  psrass1lem  18539  psrlidm  18565  psrridm  18566  mvrf1  18587  mplmon2mul  18662  evlslem1  18676  evlseu  18677  evlssca  18683  evlsvar  18684  coe1pwmul  18810  pf1ind  18881  prmirredlem  19001  mulgrhm2  19007  chrrhm  19039  znidomb  19069  psgnghm  19085  psgninv  19087  zrhpsgnodpm  19097  evpmodpmf1o  19101  psgndiflemB  19105  ip0r  19141  ipdir  19143  ipdi  19144  ipass  19149  ipassr  19150  phlpropd  19159  ocvpj  19217  uvcresum  19288  lmimlbs  19331  gsumcom3  19361  mat0dimbas0  19428  mdetrlin  19564  mdetrsca  19565  mdetr0  19567  mdetunilem8  19581  mdetuni0  19583  mdetmul  19585  maducoeval2  19602  madurid  19606  madulid  19607  matinv  19639  matunit  19640  slesolinv  19642  slesolinvbi  19643  cpmadugsumlemF  19837  restin  20119  cncmp  20344  cmpsublem  20351  conndisj  20368  cnconn  20374  kgencmp2  20498  ufldom  20914  tgplacthmeo  21055  ghmcnp  21066  qustgpopn  21071  qustgphaus  21074  tsmsxplem2  21105  tususp  21224  xpsdsval  21333  blpnfctr  21388  xmssym  21417  ressxms  21477  isngp2  21548  ngppropd  21582  nminvr  21609  blcvx  21753  icccvx  21915  pcohtpylem  21987  pcohtpy  21988  cvsmuleqdivd  22079  cvsdiveqd  22080  pjthlem1  22328  ovollb2lem  22378  ovolicc2lem1  22407  ovolicc2lem5  22412  volsup  22446  ovolioo  22458  uniiccdif  22472  uniioombllem3  22480  uniioombllem4  22481  vitalilem3  22505  itg1sub  22604  itg2const  22635  iblcnlem1  22682  itgcnlem  22684  itgaddlem2  22718  itgsub  22720  itgabs  22729  ditgsplit  22753  dvmulbr  22830  dvcmul  22835  dvcmulf  22836  dvrec  22846  dvmptres3  22847  dvmptadd  22851  dvmptmul  22852  dvmptres2  22853  dvmptneg  22857  dvmptsub  22858  dvmptcj  22859  dvmptco  22863  dveflem  22868  dvlip  22882  dvlipcn  22883  dvlip2  22884  dvcvx  22909  dvfsumle  22910  dvfsumabs  22912  dvfsumlem1  22915  dvfsumlem2  22916  ftc2  22933  ftc2ditglem  22934  itgparts  22936  itgsubstlem  22937  itgsubst  22938  fta1glem1  23053  fta1blem  23056  plyeq0lem  23101  plymullem1  23105  coeeulem  23115  coe0  23147  coesub  23148  dvply1  23174  plydivlem4  23186  plyrem  23195  fta1lem  23197  vieta1  23202  plyexmo  23203  elqaalem2  23210  elqaalem2OLD  23213  aareccl  23219  aannenlem1  23221  aaliou3lem2  23236  dvtaylp  23262  taylthlem1  23265  radcnvlem1  23305  pserdvlem2  23320  efcvx  23341  ptolemy  23388  tangtx  23397  efif1olem3  23430  efif1olem4  23431  efabl  23436  lognegb  23476  efiarg  23493  cosargd  23494  tanarg  23505  logtayl  23542  cxpneg  23563  cxpsub  23564  cxprec  23568  cxproot  23572  cxpsqrt  23585  cxpcn3lem  23624  cxpaddlelem  23628  abscxpbnd  23630  root1eq1  23632  cxpeq  23634  logrec  23637  isosctrlem2  23685  isosctrlem3  23686  isosctr  23687  ssscongptld  23688  chordthmlem  23695  heron  23701  quad2  23702  dcubic1lem  23706  mcubic  23710  cubic2  23711  cubic  23712  dquartlem2  23715  dquart  23716  quart1lem  23718  quart1  23719  asinlem2  23732  asinlem3  23734  asinsin  23755  sinacos  23768  atanlogsublem  23778  efiatan2  23780  2efiatan  23781  tanatan  23782  atantan  23786  atans2  23794  dvatan  23798  atantayl  23800  atantayl2  23801  log2cnv  23807  rlimcnp2  23829  cxplim  23834  cxp2lim  23839  cvxcl  23847  scvxcvx  23848  zetacvg  23877  lgamgulmlem4  23894  lgamcvg2  23917  gamp1  23920  wilthlem1  23930  wilthlem2  23931  ftalem5  23938  ftalem5OLD  23940  basellem3  23946  basellem5  23948  basellem8  23951  mumullem2  24044  musum  24057  musumsum  24058  muinv  24059  sgmppw  24062  1sgmprm  24064  1sgm2ppw  24065  ppiub  24069  logfac2  24082  chpchtsum  24084  perfectlem1  24094  perfectlem2  24095  dchrn0  24115  dchrfi  24120  dchrabs  24125  dchrptlem1  24129  dchrhash  24136  dchr2sum  24138  sum2dchr  24139  bposlem6  24154  bposlem9  24157  lgsvalmod  24180  lgsdilem  24187  lgsne0  24198  lgssq  24200  lgssq2  24201  lgsqr  24211  lgsdchrval  24212  lgsdchr  24213  lgseisenlem1  24214  lgseisenlem2  24215  lgseisenlem4  24217  lgsquadlem1  24219  lgsquadlem3  24221  lgsquad3  24226  m1lgs  24227  rplogsumlem1  24259  rplogsumlem2  24260  dchrisumlem2  24265  dchrisum0fno1  24286  rpvmasum2  24287  dchrisum0lem1  24291  dchrisum0lem2  24293  mudivsum  24305  mulog2sumlem1  24309  vmalogdivsum  24314  2vmadivsumlem  24315  logsqvma  24317  selberglem2  24321  selberg2lem  24325  selberg3lem1  24332  selberg4lem1  24335  selberg4  24336  pntrsumo1  24340  selbergr  24343  selberg34r  24346  pntrlog2bndlem3  24354  pntrlog2bndlem4  24355  pntibndlem2  24366  pntlemg  24373  pntlemr  24377  pntlemf  24380  ostthlem1  24402  padicabvcxp  24407  ostth3  24413  tgcgrcomlr  24461  tgifscgr  24490  iscgrglt  24496  tgbtwnconn1lem2  24555  tgbtwnconn1lem3  24556  mirne  24649  miduniq2  24669  krippenlem  24672  ragcgr  24689  cgrg3col4  24821  f1otrg  24838  ttgcontlem1  24852  brbtwn2  24872  axsegconlem10  24893  ax5seglem3  24898  ax5seglem6  24901  axpaschlem  24907  axeuclidlem  24929  axcontlem2  24932  axcontlem7  24937  axcontlem8  24938  cusgrasizeindslem3  25140  frgrancvvdeq  25707  frgrancvvdgeq  25708  numclwwlk7  25779  grpoidinvlem1  25869  grpoideu  25874  grporcan  25886  grpolcan  25898  grpoasscan1  25902  grpoinvop  25906  grpopnpcan2  25918  gxsuc  25937  gxsub  25941  gxmul  25943  ablo4  25952  subgoinv  25973  ablomul  26020  ghgrpOLD  26033  ghabloOLD  26034  rngolz  26066  rngorz  26067  zerdivemp1  26099  nvadd12  26179  nvscom  26187  nvmul0or  26210  nvz0  26234  smcnlem  26270  ipidsq  26286  sspz  26311  lno0  26334  lnoadd  26336  lnomul  26338  ipasslem3  26411  dipdi  26421  dipassr  26424  dipsubdi  26427  ubthlem2  26450  hvmul0or  26615  hvadd12  26625  hvadd4  26626  hvmulcom  26633  normneg  26734  pjhthlem1  26981  chj12  27124  spanunsni  27169  5oalem2  27245  3oalem2  27253  hoadd4  27374  homul12  27395  hosubdi  27398  honegsubdi  27400  hosub4  27403  adj2  27524  lnopmul  27557  lnopaddi  27561  lnfnaddi  27633  lnfnmuli  27634  cnlnadjlem6  27662  adjeq0  27681  leopmul  27724  opsqrlem1  27730  opsqrlem6  27735  hstnmoc  27813  strlem1  27840  chirredlem3  27982  fpwrelmapffslem  28262  subeqxfrd  28266  addeqxfrd  28267  xaddeq0  28275  bcm1n  28316  divnumden2  28327  xmulcand  28336  xreceu  28337  bhmafibid1  28351  2sqmod  28355  xrsmulgzz  28386  xrge0adddir  28401  xrge0adddi  28402  abliso  28405  ogrpaddltrbid  28430  ogrpinvlt  28433  archiabllem1a  28454  archiabllem1  28456  archiabllem2c  28458  slmdvs0  28487  dvrcan5  28503  ornglmullt  28517  orngrmullt  28518  rhmunitinv  28532  mdetpmtr2  28597  madjusmdetlem1  28600  mdetlap  28605  qtophaus  28610  qqhval2lem  28732  esumpad  28823  esummulc1  28849  esumsup  28857  measxun2  28979  measssd  28984  inelcarsg  29090  carsggect  29097  carsgclctunlem2  29098  pmeasmono  29104  oddpwdc  29134  eulerpartlemgs2  29160  eulerpartlemn  29161  totprobd  29206  signstfvn  29405  signstfveq0  29413  bnj1379  29589  bnj1321  29783  subfaclim  29858  cvxscon  29913  rescon  29916  cvmliftmolem1  29951  cvmliftlem7  29961  cvmliftlem13  29966  cvmlift2lem7  29979  cvmlift3lem5  29993  elmsta  30133  msubff1  30141  mthmpps  30167  ghomf1olem  30259  bcm1nt  30319  faclim2  30330  funsseq  30355  clsun  30928  topjoin  30965  bj-bary1lem  31622  finxpreclem4  31693  ptrest  31846  poimirlem4  31851  poimirlem6  31853  poimirlem7  31854  poimirlem9  31856  poimirlem11  31858  poimirlem12  31859  poimirlem26  31873  poimirlem27  31874  itg2addnclem  31900  itg2addnclem3  31902  itgaddnclem2  31908  itgsubnc  31911  iblmulc2nc  31914  itgabsnc  31918  ftc2nc  31933  areacirclem1  31939  areacirclem4  31942  areacirc  31944  cocanfo  31951  ablo4pnp  32085  zerdivemp1x  32101  crngm4  32143  crngohomfo  32146  fsumshftdOLD  32436  lfl0  32543  lfladd  32544  lflmul  32546  eqlkr3  32579  olm11  32705  latm12  32708  cmtcomlemN  32726  omlspjN  32739  hlatj12  32848  1cvrjat  32952  dalemrotyz  33135  padd12N  33316  pmapjlln1  33332  atmod2i1  33338  pmapocjN  33407  pnonsingN  33410  pexmidN  33446  lhp2at0  33509  lhpelim  33514  ltrncnv  33623  ltrnmwOLD  33629  cdleme7c  33723  cdleme15b  33753  cdlemednpq  33777  cdleme20yOLD  33781  cdleme20m  33802  cdleme22cN  33821  cdleme22d  33822  cdleme23b  33829  cdleme30a  33857  cdleme35h  33935  cdlemeg46frv  34004  cdlemg2fv2  34079  cdlemg2l  34082  cdlemg2m  34083  cdlemg8c  34108  cdlemg10bALTN  34115  cdlemg12  34129  cdlemg13a  34130  cdlemg18c  34159  cdlemg19  34163  trlcoat  34202  cdlemg47  34215  tendo1ne0  34307  cdlemk9  34318  cdlemk9bN  34319  dia2dimlem1  34544  tendolinv  34585  tendorinv  34586  dvhlveclem  34588  doca3N  34607  dihmeetlem7N  34790  dihjatc1  34791  dihmeetlem18N  34804  dochnoncon  34871  dihjatc  34897  dihjatcclem1  34898  dihjatcclem4  34901  dochsnkr  34952  lcfl7lem  34979  lcfl8  34982  lcfl9a  34985  lclkrlem1  34986  lclkrlem2e  34991  lclkrlem2j  34996  lcfrlem1  35022  lcfrlem9  35030  lcfrlem23  35045  lcfrlem31  35053  mapd0  35145  mapdpglem21  35172  baerlem3lem1  35187  baerlem5alem1  35188  mapdindp4  35203  mapdh6gN  35222  hdmap1l6g  35297  hgmapval0  35375  hgmaprnlem1N  35379  hlhilhillem  35443  diophrw  35513  eldioph2lem1  35514  pellexlem2  35587  pellexlem6  35591  pellex  35592  pell1234qrne0  35612  pell1234qrreccl  35613  pell1qrgaplem  35632  rmxm1  35695  oddcomabszz  35705  jm2.19lem1  35757  jm3.1lem2  35786  dnnumch3  35818  pwssplit4  35860  flcidc  35953  hashgcdlem  35987  deg1mhm  35997  itgpowd  36012  radcnvrat  36576  nzprmdif  36581  hashnzfz  36582  dvsconst  36592  dvsid  36593  expgrowth  36597  bccm1k  36604  bccn1  36606  binomcxplemnotnn0  36618  subadd4b  37389  sumnnodd  37593  icccncfext  37648  dvresntr  37671  itgsinexplem1  37713  itgsinexp  37714  stoweidlem1  37744  wallispi2lem2  37817  stirlinglem3  37821  stirlinglem5  37823  stirlinglem10  37828  stirlinglem15  37833  dirkertrigeqlem3  37845  dirkercncflem2  37849  fourierdlem26  37878  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem66  37919  fourierdlem73  37926  fourierdlem81  37934  fourierdlem83  37936  fourierdlem107  37960  etransclem23  38005  sigaradd  38289  cevathlem1  38290  m1mod0mod1  38536  mod2eq1n2dvds  38538  perfectALTVlem1  38656  perfectALTVlem2  38657  proththd  38727  imarnf1pr  38822  cusgrsizeindslem  39240  usgrauvtxvd  39263  rnglz  39475  pw2m1lepw2m1  39911  nnpw2pmod  39987  dignn0flhalflem1  40019  aacllem  40133
  Copyright terms: Public domain W3C validator