Theorem 3eqtr4d 2281

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4d.1	|- ( ph -> A = B )
3eqtr4d.2	|- ( ph -> C = A )
3eqtr4d.3	|- ( ph -> D = B )

Assertion

Ref	Expression
3eqtr4d	|- ( ph -> C = D )

Proof of Theorem 3eqtr4d

Step	Hyp	Ref	Expression
1		3eqtr4d.2	. 2 |- ( ph -> C = A )
2		3eqtr4d.3	. . 3 |- ( ph -> D = B )
3		3eqtr4d.1	. . 3 |- ( ph -> A = B )
4	2, 3	eqtr4d 2274	. 2 |- ( ph -> D = A )
5	1, 4	eqtr4d 2274	1 |- ( ph -> C = D )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  fnsnfv  5762  fvco2  5774  resfunexg  5936  fcof1  5989  fliftfun  6002  caovdir2d  6266  caov32d  6270  caov31d  6272  caov4d  6274  caovlem2d  6282  f1o3d  6298  caofcom  6333  caofdig  6336  cnvf1olem  6460  tfrlem1  6579  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  frecrdg  6679  oav2  6736  omv2  6738  omsuc  6745  nnmsucr  6761  ecovicom  6917  ecoviass  6919  ecovidi  6921  nnnninfeq  7468  nninfwlpoimlemg  7515  carden2bex  7535  addcompig  7696  addasspig  7697  mulcompig  7698  mulasspig  7699  distrpig  7700  addassnqg  7749  addnq0mo  7814  mulnq0mo  7815  nqnq0a  7821  nqnq0m  7822  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  addcmpblnr  8106  mulcmpblnrlemg  8107  addsrmo  8110  mulsrmo  8111  ltsrprg  8114  recexgt0sr  8140  mulgt0sr  8145  mulextsr1lem  8147  addcnsrec  8209  mulcnsrec  8210  pitonnlem2  8214  recidpirqlemcalc  8224  axaddcom  8237  adddir  8317  mul32  8457  mul31  8458  add32  8486  add4  8488  sub32  8561  sub4  8572  subdir  8714  mulneg2  8724  mulreim  8934  apadd1  8938  apneg  8941  divassap  9022  divdirap  9029  divmul13ap  9047  divmul24ap  9048  divdiv32ap  9052  conjmulap  9061  zeo  9755  xaddcom  10273  xnegdi  10280  xaddass  10281  xaddass2  10282  xpncan  10283  xadd4d  10297  lincmb01cmp  10415  iccf1o  10417  flhalf  10750  modqvalp1  10793  modqdi  10842  modqsubdir  10843  frecuzrdgg  10866  seq3shft2  10931  seqshft2g  10932  seq3caopr3  10941  seqcaopr3g  10942  seq3caopr  10945  seqcaoprg  10946  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seqf1oglem2a  10968  seqf1oglem2  10970  seqf1og  10971  seq3homo  10977  seqfeq3  10979  seqhomog  10980  seqfeq4g  10981  seq3distr  10982  expp1  10996  expnegap0  10997  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  sqneg  11048  sqdivap  11053  subsq2  11097  binom2  11101  modqexp  11117  facp1  11182  bcm1k  11212  bcp1n  11213  bcval5  11215  omgadd  11256  hashun  11259  hashxp  11281  hashfibclem  11296  hashf1  11301  csbwrdg  11348  ccatass  11390  lswccatn0lsw  11393  swrdlsw  11455  swrdswrd  11491  wrd2ind  11509  swrdccatin1  11511  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatpfx1  11522  swrdccat3blem  11525  cats1catd  11554  shftfibg  11599  shftfib  11602  shftval  11604  2shfti  11610  seq3shft  11617  crre  11636  remim  11639  mulreap  11643  reneg  11647  readd  11648  remullem  11650  redivap  11653  imneg  11655  imadd  11656  imdivap  11660  cjcj  11662  cjadd  11663  cjmulrcl  11666  cjneg  11669  imval2  11673  resqrexlemcalc1  11794  absneg  11830  sqabsadd  11835  sqabssub  11836  absmul  11849  absresq  11859  absexp  11860  absexpzap  11861  bdtrilem  12021  xrmaxiflemcom  12031  xrmaxadd  12043  xrminrecl  12055  xrminadd  12057  serf0  12134  summodclem3  12163  fsum3  12170  isumss  12174  fisumss  12175  fsumadd  12189  isummulc1  12210  isumdivapc  12211  fsum2dlemstep  12217  fisumcom2  12221  fisum0diag2  12230  fsummulc2  12231  fsummulc1  12232  fsumdivapc  12233  fsumconst  12237  telfsumo  12249  fsumparts  12253  binomlem  12266  isumshft  12273  arisum2  12282  geolim  12294  geo2sum  12297  geo2lim  12299  cvgratnnlemseq  12309  cvgratz  12315  mertenslem2  12319  prodfrecap  12329  prodfdivap  12330  prodmodclem2a  12359  fprodntrivap  12367  fprodssdc  12373  fprodmul  12374  fprodabs  12399  fprod2dlemstep  12405  fprodcom2fi  12409  fprodrec  12412  efcllemp  12441  efcj  12456  efexp  12465  resinval  12498  recosval  12499  cosneg  12510  efival  12515  sinadd  12519  cosadd  12520  addcos  12529  sin2t  12532  cos2t  12533  dvdsmodexp  12578  odd2np1lem  12655  oexpneg  12660  neggcd  12776  gcdabs2  12783  mulgcd  12809  mulgcdr  12811  gcddiv  12812  rplpwr  12820  eucalgval  12848  eucalginv  12850  eucalg  12853  neglcm  12869  lcmgcd  12872  mulgcddvds  12888  qredeu  12891  nn0gcdsq  12996  phimullem  13023  prmdiv  13033  coprimeprodsq  13056  pythagtriplem1  13064  pythagtriplem3  13066  pythagtriplem4  13067  pythagtriplem12  13074  pceulem  13093  pceu  13094  pcqmul  13102  pcexp  13108  pcneg  13124  pcadd  13139  pcmpt  13142  pcmpt2  13143  pcbc  13150  4sqlem7  13183  4sqlem10  13186  mul4sqlem  13192  4sqlem11  13200  ballotfilemfp1  13280  ballotfilemieq  13309  ballotfilemgun  13317  ballotfilemfrc  13319  ennnfonelemp1  13346  setsabsd  13440  setscom  13441  ressbasd  13470  strressid  13474  ressinbasd  13477  ressressg  13478  ressplusgd  13532  imasival  13676  qusin  13696  fvprif  13713  xpsfeq  13715  grpidpropdg  13743  gzsumress  13761  mnd32g  13789  mnd4g  13791  imasmnd2  13808  0mhm  13842  resmhm  13843  mhmco  13846  gzsumwmhm  13852  grpinvcnv  13922  grpinvpropdg  13929  grpinvsub  13936  grpaddsubass  13944  grpsubpropdg  13958  grpsubpropd2  13959  imasgrp2  13962  imasgrp  13963  qusgrp2  13965  mulgnnp1  13982  mulgnegnn  13984  mulgaddcom  13998  mulginvcom  13999  mulgnndir  14003  mulgnn0ass  14010  mhmmulg  14015  mulgpropdg  14016  submmulg  14018  subginv  14033  subgsub  14038  subgmulg  14040  eqglact  14077  ghmsub  14103  ghmmulg  14108  resghm  14112  ghmeql  14119  conjghm  14128  ablsub4  14166  ablsub32  14175  imasabl  14189  gzsumreidx  14190  gzsumconst  14192  gzsumshift  14198  gsumvalfi  14201  gsumf1ofi  14209  gsummptfidmadd  14210  gsummhmfi  14213  gsumconstcmn  14215  gsumressfi  14216  prdsval  14222  prdssgrpd  14240  prdsidlem  14242  prdsmndd  14243  prdsinvlem  14245  pwsplusgval  14257  pwsmulrval  14258  pws0g  14262  pwsinvg  14264  pwssub  14265  mgpress  14279  rngsubdi  14299  rngsubdir  14300  imasrng  14304  dfur2g  14315  srgass  14324  srgmulgass  14342  srgpcomp  14343  srglmhm  14346  srgrmhm  14347  crngcom  14367  ringass  14369  ringcom  14385  ringsubdi  14410  ringsubdir  14411  mulgass2  14412  ringlghm  14415  ringrghm  14416  imasring  14418  opprrng  14431  opprring  14433  oppr0g  14436  oppr1g  14437  opprnegg  14438  mulgass3  14440  dvdsrvald  14449  unitlinv  14482  unitrinv  14483  dvrfvald  14489  dvrass  14495  dvrdir  14499  rdivmuldivd  14500  rngidpropdg  14502  dvdsrpropdg  14503  unitpropdg  14504  invrpropdg  14505  rhm1  14523  rhmopp  14532  subrguss  14593  subrginv  14594  subrgdv  14595  rrgsupp  14623  aprprop  14650  opprdrng  14669  lmodcom  14719  lmodsubdir  14731  rmodislmod  14737  lsppropd  14818  srascag  14828  sravscag  14829  ixpsnbasval  14852  rsp0  14879  lidlrsppropdg  14881  rnglidlmsgrp  14883  gsumfsum  14972  expghmap  14991  mulgghm2  14992  mulgrhm  14993  zlmlemg  15012  zlmsca  15016  znle  15021  asclghm  15074  ascldimul  15080  assamulgscmlem1  15090  psrbasg  15114  psrplusgg  15118  psrlinv  15124  tgdom  15222  txbasval  15417  cnmpt11  15433  cnmpt21  15441  setsmsbasg  15629  bdbl  15653  dvmulxxbr  15852  dvimulf  15856  dvcj  15859  dvfre  15860  dvrecap  15863  dvmptc  15867  dvmptfsum  15875  dvef  15877  plyaddlem1  15897  plyrecj  15913  dvply1  15915  sinperlem  15959  coshalfpip  15973  ptolemy  15975  tangtx  15989  relogef  16015  logfac  16048  rpcxpadd  16060  rpmulcxp  16064  rpdivcxp  16066  cxpmul  16067  rpcxpmul2  16068  abscxp  16070  rpcxpsqrt  16077  rpabscxpbnd  16095  rplogbreexp  16108  rprelogbmul  16110  rprelogbdiv  16112  birthdaylem2  16145  pellexlem3  16150  ppiprm  16170  ppinprm  16171  1sgmprm  16189  perfect1  16196  perfectlem2  16198  perfect  16199  bcmono  16202  lgsneg  16241  lgsmod  16243  lgsdir2  16250  lgsdirprm  16251  lgsdir  16252  lgsdi  16254  lgssq  16257  lgssq2  16258  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem6  16284  lgseisenlem1  16287  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlem1  16294  lgsquad2  16300  2sqlem3  16334  setsiedg  16391  vtxdeqd  16635  vtxdfifiun  16636  trlsegvdegfi  16806  depindlem3  16847  bj-charfundcALT  16933  nninfsellemeqinf  17157  refeq  17171