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  7469  nninfwlpoimlemg  7516  carden2bex  7536  addcompig  7697  addasspig  7698  mulcompig  7699  mulasspig  7700  distrpig  7701  addassnqg  7750  addnq0mo  7815  mulnq0mo  7816  nqnq0a  7822  nqnq0m  7823  distrnq0  7827  mulcomnq0  7828  addassnq0  7830  addcmpblnr  8107  mulcmpblnrlemg  8108  addsrmo  8111  mulsrmo  8112  ltsrprg  8115  recexgt0sr  8141  mulgt0sr  8146  mulextsr1lem  8148  addcnsrec  8210  mulcnsrec  8211  pitonnlem2  8215  recidpirqlemcalc  8225  axaddcom  8238  adddir  8318  mul32  8458  mul31  8459  add32  8487  add4  8489  sub32  8562  sub4  8573  subdir  8715  mulneg2  8725  mulreim  8935  apadd1  8939  apneg  8942  divassap  9023  divdirap  9030  divmul13ap  9048  divmul24ap  9049  divdiv32ap  9053  conjmulap  9062  zeo  9756  xaddcom  10274  xnegdi  10281  xaddass  10282  xaddass2  10283  xpncan  10284  xadd4d  10298  lincmb01cmp  10416  iccf1o  10418  flhalf  10752  modqvalp1  10795  modqdi  10844  modqsubdir  10845  frecuzrdgg  10868  seq3shft2  10933  seqshft2g  10934  seq3caopr3  10943  seqcaopr3g  10944  seq3caopr  10947  seqcaoprg  10948  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seqf1oglem2a  10970  seqf1oglem2  10972  seqf1og  10973  seq3homo  10979  seqfeq3  10981  seqhomog  10982  seqfeq4g  10983  seq3distr  10984  expp1  10998  expnegap0  10999  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  sqneg  11050  sqdivap  11055  subsq2  11099  binom2  11103  modqexp  11119  facp1  11184  bcm1k  11214  bcp1n  11215  bcval5  11217  omgadd  11258  hashun  11261  hashxp  11283  hashfibclem  11298  hashf1  11303  csbwrdg  11350  ccatass  11392  lswccatn0lsw  11395  swrdlsw  11457  swrdswrd  11493  wrd2ind  11511  swrdccatin1  11513  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatpfx1  11524  swrdccat3blem  11527  cats1catd  11556  shftfibg  11601  shftfib  11604  shftval  11606  2shfti  11612  seq3shft  11619  crre  11638  remim  11641  mulreap  11645  reneg  11649  readd  11650  remullem  11652  redivap  11655  imneg  11657  imadd  11658  imdivap  11662  cjcj  11664  cjadd  11665  cjmulrcl  11668  cjneg  11671  imval2  11675  resqrexlemcalc1  11796  absneg  11832  sqabsadd  11837  sqabssub  11838  absmul  11851  absresq  11861  absexp  11862  absexpzap  11863  bdtrilem  12024  xrmaxiflemcom  12034  xrmaxadd  12046  xrminrecl  12058  xrminadd  12060  serf0  12137  summodclem3  12166  fsum3  12173  isumss  12177  fisumss  12178  fsumadd  12192  isummulc1  12213  isumdivapc  12214  fsum2dlemstep  12220  fisumcom2  12224  fisum0diag2  12233  fsummulc2  12234  fsummulc1  12235  fsumdivapc  12236  fsumconst  12240  telfsumo  12252  fsumparts  12256  binomlem  12269  isumshft  12276  arisum2  12285  geolim  12297  geo2sum  12300  geo2lim  12302  cvgratnnlemseq  12312  cvgratz  12318  mertenslem2  12322  prodfrecap  12332  prodfdivap  12333  prodmodclem2a  12362  fprodntrivap  12370  fprodssdc  12376  fprodmul  12377  fprodabs  12402  fprod2dlemstep  12408  fprodcom2fi  12412  fprodrec  12415  efcllemp  12444  efcj  12459  efexp  12468  resinval  12501  recosval  12502  cosneg  12513  efival  12518  sinadd  12522  cosadd  12523  addcos  12532  sin2t  12535  cos2t  12536  dvdsmodexp  12581  odd2np1lem  12658  oexpneg  12663  neggcd  12779  gcdabs2  12786  mulgcd  12812  mulgcdr  12814  gcddiv  12815  rplpwr  12823  eucalgval  12851  eucalginv  12853  eucalg  12856  neglcm  12872  lcmgcd  12875  mulgcddvds  12891  qredeu  12894  nn0gcdsq  12999  phimullem  13026  prmdiv  13036  coprimeprodsq  13059  pythagtriplem1  13067  pythagtriplem3  13069  pythagtriplem4  13070  pythagtriplem12  13077  pceulem  13096  pceu  13097  pcqmul  13105  pcexp  13111  pcneg  13127  pcadd  13142  pcmpt  13145  pcmpt2  13146  pcbc  13153  4sqlem7  13186  4sqlem10  13189  mul4sqlem  13195  4sqlem11  13203  ballotfilemfp1  13283  ballotfilemieq  13312  ballotfilemgun  13320  ballotfilemfrc  13322  ennnfonelemp1  13349  setsabsd  13443  setscom  13444  ressbasd  13474  strressid  13478  ressinbasd  13481  ressressg  13482  ressplusgd  13536  imasival  13680  qusin  13700  fvprif  13717  xpsfeq  13719  grpidpropdg  13747  gzsumress  13765  mnd32g  13793  mnd4g  13795  imasmnd2  13812  0mhm  13846  resmhm  13847  mhmco  13850  gzsumwmhm  13856  grpinvcnv  13926  grpinvpropdg  13933  grpinvsub  13940  grpaddsubass  13948  grpsubpropdg  13962  grpsubpropd2  13963  imasgrp2  13966  imasgrp  13967  qusgrp2  13969  mulgnnp1  13986  mulgnegnn  13988  mulgaddcom  14002  mulginvcom  14003  mulgnndir  14007  mulgnn0ass  14014  mhmmulg  14019  mulgpropdg  14020  submmulg  14022  subginv  14037  subgsub  14042  subgmulg  14044  eqglact  14081  ghmsub  14107  ghmmulg  14112  resghm  14116  ghmeql  14123  conjghm  14132  ablsub4  14201  ablsub32  14210  imasabl  14224  gzsumreidx  14225  gzsumconst  14227  gzsumshift  14233  gsumvalfi  14236  gsumf1ofi  14244  gsummptfidmadd  14245  gsummhmfi  14248  gsumconstcmn  14250  gsumressfi  14251  prdsval  14257  prdssgrpd  14275  prdsidlem  14277  prdsmndd  14278  prdsinvlem  14280  pwsplusgval  14292  pwsmulrval  14293  pws0g  14297  pwsinvg  14299  pwssub  14300  mgpress  14314  rngsubdi  14334  rngsubdir  14335  imasrng  14339  dfur2g  14350  srgass  14359  srgmulgass  14377  srgpcomp  14378  srglmhm  14381  srgrmhm  14382  crngcom  14402  ringass  14404  ringcom  14420  ringsubdi  14445  ringsubdir  14446  mulgass2  14447  ringlghm  14450  ringrghm  14451  imasring  14453  opprrng  14466  opprring  14468  oppr0g  14471  oppr1g  14472  opprnegg  14473  mulgass3  14475  dvdsrvald  14484  unitlinv  14517  unitrinv  14518  dvrfvald  14524  dvrass  14530  dvrdir  14534  rdivmuldivd  14535  rngidpropdg  14537  dvdsrpropdg  14538  unitpropdg  14539  invrpropdg  14540  rhm1  14558  rhmopp  14567  subrguss  14628  subrginv  14629  subrgdv  14630  rrgsupp  14658  aprprop  14685  opprdrng  14704  lmodcom  14754  lmodsubdir  14766  rmodislmod  14772  lsppropd  14853  srascag  14863  sravscag  14864  ixpsnbasval  14887  rsp0  14914  lidlrsppropdg  14916  rnglidlmsgrp  14918  gsumfsum  15007  expghmap  15026  mulgghm2  15027  mulgrhm  15028  zlmlemg  15047  zlmsca  15051  znle  15056  asclghm  15109  ascldimul  15115  assamulgscmlem1  15125  psrbasg  15150  psrplusgg  15154  psrlinv  15166  tgdom  15264  txbasval  15459  cnmpt11  15475  cnmpt21  15483  setsmsbasg  15671  bdbl  15695  dvmulxxbr  15894  dvimulf  15898  dvcj  15901  dvfre  15902  dvrecap  15905  dvmptc  15909  dvmptfsum  15917  dvef  15919  plyaddlem1  15939  plyrecj  15955  dvply1  15957  sinperlem  16001  coshalfpip  16015  ptolemy  16017  tangtx  16031  relogef  16057  logfac  16090  rpcxpadd  16102  rpmulcxp  16106  rpdivcxp  16108  cxpmul  16109  rpcxpmul2  16110  abscxp  16112  rpcxpsqrt  16119  rpabscxpbnd  16137  rplogbreexp  16150  rprelogbmul  16152  rprelogbdiv  16154  birthdaylem2  16187  pellexlem3  16192  chtqfl  16219  ppiprm  16220  ppinprm  16221  chtnprm  16223  prmorcht  16243  1sgmprm  16249  perfect1  16259  perfectlem2  16261  perfect  16262  bcmono  16265  bposlem9  16280  lgsneg  16309  lgsmod  16311  lgsdir2  16318  lgsdirprm  16319  lgsdir  16320  lgsdi  16322  lgssq  16325  lgssq2  16326  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem6  16352  lgseisenlem1  16355  lgseisenlem3  16357  lgseisenlem4  16358  lgsquadlem1  16362  lgsquad2  16368  2sqlem3  16402  setsiedg  16459  vtxdeqd  16703  vtxdfifiun  16704  trlsegvdegfi  16874  depindlem3  16915  bj-charfundcALT  17001  nninfsellemeqinf  17225  refeq  17239