Theorem 3eqtr4d 2236

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

Syntax hints:   -> wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  fnsnfv  5617  fvco2  5627  resfunexg  5780  fcof1  5827  fliftfun  5840  caovdir2d  6097  caov32d  6101  caov31d  6103  caov4d  6105  caovlem2d  6113  caofcom  6158  caofdig  6161  cnvf1olem  6279  tfrlem1  6363  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  frecrdg  6463  oav2  6518  omv2  6520  omsuc  6527  nnmsucr  6543  ecovicom  6699  ecoviass  6701  ecovidi  6703  nnnninfeq  7189  nninfwlpoimlemg  7236  carden2bex  7251  addcompig  7391  addasspig  7392  mulcompig  7393  mulasspig  7394  distrpig  7395  addassnqg  7444  addnq0mo  7509  mulnq0mo  7510  nqnq0a  7516  nqnq0m  7517  distrnq0  7521  mulcomnq0  7522  addassnq0  7524  addcmpblnr  7801  mulcmpblnrlemg  7802  addsrmo  7805  mulsrmo  7806  ltsrprg  7809  recexgt0sr  7835  mulgt0sr  7840  mulextsr1lem  7842  addcnsrec  7904  mulcnsrec  7905  pitonnlem2  7909  recidpirqlemcalc  7919  axaddcom  7932  adddir  8012  mul32  8151  mul31  8152  add32  8180  add4  8182  sub32  8255  sub4  8266  subdir  8407  mulneg2  8417  mulreim  8625  apadd1  8629  apneg  8632  divassap  8711  divdirap  8718  divmul13ap  8736  divmul24ap  8737  divdiv32ap  8741  conjmulap  8750  zeo  9425  xaddcom  9930  xnegdi  9937  xaddass  9938  xaddass2  9939  xpncan  9940  xadd4d  9954  lincmb01cmp  10072  iccf1o  10073  flhalf  10374  modqvalp1  10417  modqdi  10466  modqsubdir  10467  frecuzrdgg  10490  seq3shft2  10555  seqshft2g  10556  seq3caopr3  10565  seqcaopr3g  10566  seq3caopr  10569  seqcaoprg  10570  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seqf1oglem2a  10592  seqf1oglem2  10594  seqf1og  10595  seq3homo  10601  seqfeq3  10603  seqhomog  10604  seqfeq4g  10605  seq3distr  10606  expp1  10620  expnegap0  10621  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  sqneg  10672  sqdivap  10677  subsq2  10721  binom2  10725  modqexp  10740  facp1  10804  bcm1k  10834  bcp1n  10835  bcval5  10837  omgadd  10876  hashun  10879  hashxp  10900  csbwrdg  10946  shftfibg  10967  shftfib  10970  shftval  10972  2shfti  10978  seq3shft  10985  crre  11004  remim  11007  mulreap  11011  reneg  11015  readd  11016  remullem  11018  redivap  11021  imneg  11023  imadd  11024  imdivap  11028  cjcj  11030  cjadd  11031  cjmulrcl  11034  cjneg  11037  imval2  11041  resqrexlemcalc1  11161  absneg  11197  sqabsadd  11202  sqabssub  11203  absmul  11216  absresq  11225  absexp  11226  absexpzap  11227  bdtrilem  11385  xrmaxiflemcom  11395  xrmaxadd  11407  xrminrecl  11419  xrminadd  11421  serf0  11498  summodclem3  11526  fsum3  11533  isumss  11537  fisumss  11538  fsumadd  11552  isummulc1  11573  isumdivapc  11574  fsum2dlemstep  11580  fisumcom2  11584  fisum0diag2  11593  fsummulc2  11594  fsummulc1  11595  fsumdivapc  11596  fsumconst  11600  telfsumo  11612  fsumparts  11616  binomlem  11629  isumshft  11636  arisum2  11645  geolim  11657  geo2sum  11660  geo2lim  11662  cvgratnnlemseq  11672  cvgratz  11678  mertenslem2  11682  prodfrecap  11692  prodfdivap  11693  prodmodclem2a  11722  fprodntrivap  11730  fprodssdc  11736  fprodmul  11737  fprodabs  11762  fprod2dlemstep  11768  fprodcom2fi  11772  fprodrec  11775  efcllemp  11804  efcj  11819  efexp  11828  resinval  11861  recosval  11862  cosneg  11873  efival  11878  sinadd  11882  cosadd  11883  addcos  11892  sin2t  11895  cos2t  11896  dvdsmodexp  11941  odd2np1lem  12016  oexpneg  12021  neggcd  12123  gcdabs2  12130  mulgcd  12156  mulgcdr  12158  gcddiv  12159  rplpwr  12167  eucalgval  12195  eucalginv  12197  eucalg  12200  neglcm  12216  lcmgcd  12219  mulgcddvds  12235  qredeu  12238  nn0gcdsq  12341  phimullem  12366  prmdiv  12376  coprimeprodsq  12398  pythagtriplem1  12406  pythagtriplem3  12408  pythagtriplem4  12409  pythagtriplem12  12416  pceulem  12435  pceu  12436  pcqmul  12444  pcexp  12450  pcneg  12466  pcadd  12481  pcmpt  12484  pcmpt2  12485  pcbc  12492  4sqlem7  12525  4sqlem10  12528  mul4sqlem  12534  4sqlem11  12542  ennnfonelemp1  12566  setsabsd  12660  setscom  12661  ressbasd  12688  strressid  12692  ressinbasd  12695  ressressg  12696  ressplusgd  12749  imasival  12892  qusin  12912  fvprif  12929  xpsfeq  12931  grpidpropdg  12960  gsumpropd  12978  gsumpropd2  12979  gsumress  12981  mnd32g  13011  mnd4g  13013  0mhm  13061  resmhm  13062  mhmco  13065  gsumwmhm  13073  grpinvcnv  13143  grpinvpropdg  13150  grpinvsub  13157  grpaddsubass  13165  grpsubpropdg  13179  grpsubpropd2  13180  imasgrp2  13183  imasgrp  13184  qusgrp2  13186  mulgnnp1  13203  mulgnegnn  13205  mulgaddcom  13219  mulginvcom  13220  mulgnndir  13224  mulgnn0ass  13231  mhmmulg  13236  mulgpropdg  13237  submmulg  13239  subginv  13254  subgsub  13259  subgmulg  13261  eqglact  13298  ghmsub  13324  ghmmulg  13329  resghm  13333  ghmeql  13340  conjghm  13349  ablsub4  13386  ablsub32  13395  imasabl  13409  gsumfzreidx  13410  gsumfzmptfidmadd  13412  gsumfzconst  13414  mgpress  13430  rngsubdi  13450  rngsubdir  13451  imasrng  13455  dfur2g  13461  srgass  13470  srgmulgass  13488  srgpcomp  13489  srglmhm  13492  srgrmhm  13493  crngcom  13513  ringass  13515  ringcom  13530  ringsubdi  13555  ringsubdir  13556  mulgass2  13557  ringlghm  13560  ringrghm  13561  imasring  13563  opprrng  13576  opprring  13578  oppr0g  13580  oppr1g  13581  opprnegg  13582  mulgass3  13584  dvdsrvald  13592  unitlinv  13625  unitrinv  13626  dvrfvald  13632  dvrass  13638  dvrdir  13642  rdivmuldivd  13643  rngidpropdg  13645  dvdsrpropdg  13646  unitpropdg  13647  invrpropdg  13648  rhm1  13666  rhmopp  13675  subrguss  13735  subrginv  13736  subrgdv  13737  lmodcom  13832  lmodsubdir  13844  rmodislmod  13850  lsppropd  13931  srascag  13941  sravscag  13942  ixpsnbasval  13965  rsp0  13992  lidlrsppropdg  13994  rnglidlmsgrp  13996  gsumfzfsumlemm  14086  expghmap  14106  mulgghm2  14107  mulgrhm  14108  zlmlemg  14127  zlmsca  14131  znle  14136  psrbasg  14170  psrplusgg  14173  tgdom  14251  txbasval  14446  cnmpt11  14462  cnmpt21  14470  setsmsbasg  14658  bdbl  14682  dvmulxxbr  14881  dvimulf  14885  dvcj  14888  dvfre  14889  dvrecap  14892  dvmptc  14896  dvmptfsum  14904  dvef  14906  plyaddlem1  14926  plyrecj  14941  dvply1  14943  sinperlem  14984  coshalfpip  14998  ptolemy  15000  tangtx  15014  relogef  15040  rpcxpadd  15081  rpmulcxp  15085  rpdivcxp  15087  cxpmul  15088  abscxp  15090  rpcxpsqrt  15097  rpabscxpbnd  15114  rplogbreexp  15126  rprelogbmul  15128  rprelogbdiv  15130  lgsneg  15181  lgsmod  15183  lgsdir2  15190  lgsdirprm  15191  lgsdir  15192  lgsdi  15194  lgssq  15197  lgssq2  15198  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem6  15224  lgseisenlem1  15227  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquad2  15240  2sqlem3  15274  bj-charfundcALT  15371  nninfsellemeqinf  15576  refeq  15588