Theorem 3eqtr4d 2248

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 2241	. 2 |- ( ph -> D = A )
5	1, 4	eqtr4d 2241	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  fnsnfv  5640  fvco2  5650  resfunexg  5807  fcof1  5854  fliftfun  5867  caovdir2d  6125  caov32d  6129  caov31d  6131  caov4d  6133  caovlem2d  6141  caofcom  6191  caofdig  6194  cnvf1olem  6312  tfrlem1  6396  tfrlemisucaccv  6413  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  frecrdg  6496  oav2  6551  omv2  6553  omsuc  6560  nnmsucr  6576  ecovicom  6732  ecoviass  6734  ecovidi  6736  nnnninfeq  7232  nninfwlpoimlemg  7279  carden2bex  7299  addcompig  7444  addasspig  7445  mulcompig  7446  mulasspig  7447  distrpig  7448  addassnqg  7497  addnq0mo  7562  mulnq0mo  7563  nqnq0a  7569  nqnq0m  7570  distrnq0  7574  mulcomnq0  7575  addassnq0  7577  addcmpblnr  7854  mulcmpblnrlemg  7855  addsrmo  7858  mulsrmo  7859  ltsrprg  7862  recexgt0sr  7888  mulgt0sr  7893  mulextsr1lem  7895  addcnsrec  7957  mulcnsrec  7958  pitonnlem2  7962  recidpirqlemcalc  7972  axaddcom  7985  adddir  8065  mul32  8204  mul31  8205  add32  8233  add4  8235  sub32  8308  sub4  8319  subdir  8460  mulneg2  8470  mulreim  8679  apadd1  8683  apneg  8686  divassap  8765  divdirap  8772  divmul13ap  8790  divmul24ap  8791  divdiv32ap  8795  conjmulap  8804  zeo  9480  xaddcom  9985  xnegdi  9992  xaddass  9993  xaddass2  9994  xpncan  9995  xadd4d  10009  lincmb01cmp  10127  iccf1o  10128  flhalf  10447  modqvalp1  10490  modqdi  10539  modqsubdir  10540  frecuzrdgg  10563  seq3shft2  10628  seqshft2g  10629  seq3caopr3  10638  seqcaopr3g  10639  seq3caopr  10642  seqcaoprg  10643  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  seqf1oglem2a  10665  seqf1oglem2  10667  seqf1og  10668  seq3homo  10674  seqfeq3  10676  seqhomog  10677  seqfeq4g  10678  seq3distr  10679  expp1  10693  expnegap0  10694  expaddzaplem  10729  expaddzap  10730  expmulzap  10732  sqneg  10745  sqdivap  10750  subsq2  10794  binom2  10798  modqexp  10813  facp1  10877  bcm1k  10907  bcp1n  10908  bcval5  10910  omgadd  10949  hashun  10952  hashxp  10973  csbwrdg  11025  ccatass  11067  lswccatn0lsw  11070  swrdlsw  11125  shftfibg  11164  shftfib  11167  shftval  11169  2shfti  11175  seq3shft  11182  crre  11201  remim  11204  mulreap  11208  reneg  11212  readd  11213  remullem  11215  redivap  11218  imneg  11220  imadd  11221  imdivap  11225  cjcj  11227  cjadd  11228  cjmulrcl  11231  cjneg  11234  imval2  11238  resqrexlemcalc1  11358  absneg  11394  sqabsadd  11399  sqabssub  11400  absmul  11413  absresq  11422  absexp  11423  absexpzap  11424  bdtrilem  11583  xrmaxiflemcom  11593  xrmaxadd  11605  xrminrecl  11617  xrminadd  11619  serf0  11696  summodclem3  11724  fsum3  11731  isumss  11735  fisumss  11736  fsumadd  11750  isummulc1  11771  isumdivapc  11772  fsum2dlemstep  11778  fisumcom2  11782  fisum0diag2  11791  fsummulc2  11792  fsummulc1  11793  fsumdivapc  11794  fsumconst  11798  telfsumo  11810  fsumparts  11814  binomlem  11827  isumshft  11834  arisum2  11843  geolim  11855  geo2sum  11858  geo2lim  11860  cvgratnnlemseq  11870  cvgratz  11876  mertenslem2  11880  prodfrecap  11890  prodfdivap  11891  prodmodclem2a  11920  fprodntrivap  11928  fprodssdc  11934  fprodmul  11935  fprodabs  11960  fprod2dlemstep  11966  fprodcom2fi  11970  fprodrec  11973  efcllemp  12002  efcj  12017  efexp  12026  resinval  12059  recosval  12060  cosneg  12071  efival  12076  sinadd  12080  cosadd  12081  addcos  12090  sin2t  12093  cos2t  12094  dvdsmodexp  12139  odd2np1lem  12216  oexpneg  12221  neggcd  12337  gcdabs2  12344  mulgcd  12370  mulgcdr  12372  gcddiv  12373  rplpwr  12381  eucalgval  12409  eucalginv  12411  eucalg  12414  neglcm  12430  lcmgcd  12433  mulgcddvds  12449  qredeu  12452  nn0gcdsq  12555  phimullem  12580  prmdiv  12590  coprimeprodsq  12613  pythagtriplem1  12621  pythagtriplem3  12623  pythagtriplem4  12624  pythagtriplem12  12631  pceulem  12650  pceu  12651  pcqmul  12659  pcexp  12665  pcneg  12681  pcadd  12696  pcmpt  12699  pcmpt2  12700  pcbc  12707  4sqlem7  12740  4sqlem10  12743  mul4sqlem  12749  4sqlem11  12757  ennnfonelemp1  12810  setsabsd  12904  setscom  12905  ressbasd  12932  strressid  12936  ressinbasd  12939  ressressg  12940  ressplusgd  12994  prdsval  13138  pwsplusgval  13160  pwsmulrval  13161  imasival  13171  qusin  13191  fvprif  13208  xpsfeq  13210  grpidpropdg  13239  gsumpropd  13257  gsumpropd2  13258  gsumress  13260  prdssgrpd  13280  mnd32g  13292  mnd4g  13294  prdsidlem  13312  prdsmndd  13313  pws0g  13316  imasmnd2  13317  0mhm  13351  resmhm  13352  mhmco  13355  gsumwmhm  13363  grpinvcnv  13433  grpinvpropdg  13440  grpinvsub  13447  grpaddsubass  13455  grpsubpropdg  13469  grpsubpropd2  13470  prdsinvlem  13473  pwsinvg  13477  pwssub  13478  imasgrp2  13479  imasgrp  13480  qusgrp2  13482  mulgnnp1  13499  mulgnegnn  13501  mulgaddcom  13515  mulginvcom  13516  mulgnndir  13520  mulgnn0ass  13527  mhmmulg  13532  mulgpropdg  13533  submmulg  13535  subginv  13550  subgsub  13555  subgmulg  13557  eqglact  13594  ghmsub  13620  ghmmulg  13625  resghm  13629  ghmeql  13636  conjghm  13645  ablsub4  13682  ablsub32  13691  imasabl  13705  gsumfzreidx  13706  gsumfzmptfidmadd  13708  gsumfzconst  13710  mgpress  13726  rngsubdi  13746  rngsubdir  13747  imasrng  13751  dfur2g  13757  srgass  13766  srgmulgass  13784  srgpcomp  13785  srglmhm  13788  srgrmhm  13789  crngcom  13809  ringass  13811  ringcom  13826  ringsubdi  13851  ringsubdir  13852  mulgass2  13853  ringlghm  13856  ringrghm  13857  imasring  13859  opprrng  13872  opprring  13874  oppr0g  13876  oppr1g  13877  opprnegg  13878  mulgass3  13880  dvdsrvald  13888  unitlinv  13921  unitrinv  13922  dvrfvald  13928  dvrass  13934  dvrdir  13938  rdivmuldivd  13939  rngidpropdg  13941  dvdsrpropdg  13942  unitpropdg  13943  invrpropdg  13944  rhm1  13962  rhmopp  13971  subrguss  14031  subrginv  14032  subrgdv  14033  lmodcom  14128  lmodsubdir  14140  rmodislmod  14146  lsppropd  14227  srascag  14237  sravscag  14238  ixpsnbasval  14261  rsp0  14288  lidlrsppropdg  14290  rnglidlmsgrp  14292  gsumfzfsumlemm  14382  expghmap  14402  mulgghm2  14403  mulgrhm  14404  zlmlemg  14423  zlmsca  14427  znle  14432  psrbasg  14469  psrplusgg  14473  psrlinv  14479  tgdom  14577  txbasval  14772  cnmpt11  14788  cnmpt21  14796  setsmsbasg  14984  bdbl  15008  dvmulxxbr  15207  dvimulf  15211  dvcj  15214  dvfre  15215  dvrecap  15218  dvmptc  15222  dvmptfsum  15230  dvef  15232  plyaddlem1  15252  plyrecj  15268  dvply1  15270  sinperlem  15313  coshalfpip  15327  ptolemy  15329  tangtx  15343  relogef  15369  rpcxpadd  15410  rpmulcxp  15414  rpdivcxp  15416  cxpmul  15417  rpcxpmul2  15418  abscxp  15420  rpcxpsqrt  15427  rpabscxpbnd  15445  rplogbreexp  15458  rprelogbmul  15460  rprelogbdiv  15462  1sgmprm  15499  perfect1  15503  perfectlem2  15505  perfect  15506  lgsneg  15534  lgsmod  15536  lgsdir2  15543  lgsdirprm  15544  lgsdir  15545  lgsdi  15547  lgssq  15550  lgssq2  15551  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem6  15577  lgseisenlem1  15580  lgseisenlem3  15582  lgseisenlem4  15583  lgsquadlem1  15587  lgsquad2  15593  2sqlem3  15627  bj-charfundcALT  15782  nninfsellemeqinf  15990  refeq  16004