Theorem 3eqtr4d 2272

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  fnsnfv  5693  fvco2  5703  resfunexg  5860  fcof1  5907  fliftfun  5920  caovdir2d  6182  caov32d  6186  caov31d  6188  caov4d  6190  caovlem2d  6198  caofcom  6249  caofdig  6252  cnvf1olem  6370  tfrlem1  6454  tfrlemisucaccv  6471  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  frecrdg  6554  oav2  6609  omv2  6611  omsuc  6618  nnmsucr  6634  ecovicom  6790  ecoviass  6792  ecovidi  6794  nnnninfeq  7295  nninfwlpoimlemg  7342  carden2bex  7362  addcompig  7516  addasspig  7517  mulcompig  7518  mulasspig  7519  distrpig  7520  addassnqg  7569  addnq0mo  7634  mulnq0mo  7635  nqnq0a  7641  nqnq0m  7642  distrnq0  7646  mulcomnq0  7647  addassnq0  7649  addcmpblnr  7926  mulcmpblnrlemg  7927  addsrmo  7930  mulsrmo  7931  ltsrprg  7934  recexgt0sr  7960  mulgt0sr  7965  mulextsr1lem  7967  addcnsrec  8029  mulcnsrec  8030  pitonnlem2  8034  recidpirqlemcalc  8044  axaddcom  8057  adddir  8137  mul32  8276  mul31  8277  add32  8305  add4  8307  sub32  8380  sub4  8391  subdir  8532  mulneg2  8542  mulreim  8751  apadd1  8755  apneg  8758  divassap  8837  divdirap  8844  divmul13ap  8862  divmul24ap  8863  divdiv32ap  8867  conjmulap  8876  zeo  9552  xaddcom  10057  xnegdi  10064  xaddass  10065  xaddass2  10066  xpncan  10067  xadd4d  10081  lincmb01cmp  10199  iccf1o  10200  flhalf  10522  modqvalp1  10565  modqdi  10614  modqsubdir  10615  frecuzrdgg  10638  seq3shft2  10703  seqshft2g  10704  seq3caopr3  10713  seqcaopr3g  10714  seq3caopr  10717  seqcaoprg  10718  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seqf1oglem2a  10740  seqf1oglem2  10742  seqf1og  10743  seq3homo  10749  seqfeq3  10751  seqhomog  10752  seqfeq4g  10753  seq3distr  10754  expp1  10768  expnegap0  10769  expaddzaplem  10804  expaddzap  10805  expmulzap  10807  sqneg  10820  sqdivap  10825  subsq2  10869  binom2  10873  modqexp  10888  facp1  10952  bcm1k  10982  bcp1n  10983  bcval5  10985  omgadd  11024  hashun  11027  hashxp  11048  csbwrdg  11101  ccatass  11143  lswccatn0lsw  11146  swrdlsw  11201  swrdswrd  11237  wrd2ind  11255  swrdccatin1  11257  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccatpfx1  11268  swrdccat3blem  11271  cats1catd  11300  shftfibg  11331  shftfib  11334  shftval  11336  2shfti  11342  seq3shft  11349  crre  11368  remim  11371  mulreap  11375  reneg  11379  readd  11380  remullem  11382  redivap  11385  imneg  11387  imadd  11388  imdivap  11392  cjcj  11394  cjadd  11395  cjmulrcl  11398  cjneg  11401  imval2  11405  resqrexlemcalc1  11525  absneg  11561  sqabsadd  11566  sqabssub  11567  absmul  11580  absresq  11589  absexp  11590  absexpzap  11591  bdtrilem  11750  xrmaxiflemcom  11760  xrmaxadd  11772  xrminrecl  11784  xrminadd  11786  serf0  11863  summodclem3  11891  fsum3  11898  isumss  11902  fisumss  11903  fsumadd  11917  isummulc1  11938  isumdivapc  11939  fsum2dlemstep  11945  fisumcom2  11949  fisum0diag2  11958  fsummulc2  11959  fsummulc1  11960  fsumdivapc  11961  fsumconst  11965  telfsumo  11977  fsumparts  11981  binomlem  11994  isumshft  12001  arisum2  12010  geolim  12022  geo2sum  12025  geo2lim  12027  cvgratnnlemseq  12037  cvgratz  12043  mertenslem2  12047  prodfrecap  12057  prodfdivap  12058  prodmodclem2a  12087  fprodntrivap  12095  fprodssdc  12101  fprodmul  12102  fprodabs  12127  fprod2dlemstep  12133  fprodcom2fi  12137  fprodrec  12140  efcllemp  12169  efcj  12184  efexp  12193  resinval  12226  recosval  12227  cosneg  12238  efival  12243  sinadd  12247  cosadd  12248  addcos  12257  sin2t  12260  cos2t  12261  dvdsmodexp  12306  odd2np1lem  12383  oexpneg  12388  neggcd  12504  gcdabs2  12511  mulgcd  12537  mulgcdr  12539  gcddiv  12540  rplpwr  12548  eucalgval  12576  eucalginv  12578  eucalg  12581  neglcm  12597  lcmgcd  12600  mulgcddvds  12616  qredeu  12619  nn0gcdsq  12722  phimullem  12747  prmdiv  12757  coprimeprodsq  12780  pythagtriplem1  12788  pythagtriplem3  12790  pythagtriplem4  12791  pythagtriplem12  12798  pceulem  12817  pceu  12818  pcqmul  12826  pcexp  12832  pcneg  12848  pcadd  12863  pcmpt  12866  pcmpt2  12867  pcbc  12874  4sqlem7  12907  4sqlem10  12910  mul4sqlem  12916  4sqlem11  12924  ennnfonelemp1  12977  setsabsd  13071  setscom  13072  ressbasd  13100  strressid  13104  ressinbasd  13107  ressressg  13108  ressplusgd  13162  prdsval  13306  pwsplusgval  13328  pwsmulrval  13329  imasival  13339  qusin  13359  fvprif  13376  xpsfeq  13378  grpidpropdg  13407  gsumpropd  13425  gsumpropd2  13426  gsumress  13428  prdssgrpd  13448  mnd32g  13460  mnd4g  13462  prdsidlem  13480  prdsmndd  13481  pws0g  13484  imasmnd2  13485  0mhm  13519  resmhm  13520  mhmco  13523  gsumwmhm  13531  grpinvcnv  13601  grpinvpropdg  13608  grpinvsub  13615  grpaddsubass  13623  grpsubpropdg  13637  grpsubpropd2  13638  prdsinvlem  13641  pwsinvg  13645  pwssub  13646  imasgrp2  13647  imasgrp  13648  qusgrp2  13650  mulgnnp1  13667  mulgnegnn  13669  mulgaddcom  13683  mulginvcom  13684  mulgnndir  13688  mulgnn0ass  13695  mhmmulg  13700  mulgpropdg  13701  submmulg  13703  subginv  13718  subgsub  13723  subgmulg  13725  eqglact  13762  ghmsub  13788  ghmmulg  13793  resghm  13797  ghmeql  13804  conjghm  13813  ablsub4  13850  ablsub32  13859  imasabl  13873  gsumfzreidx  13874  gsumfzmptfidmadd  13876  gsumfzconst  13878  mgpress  13894  rngsubdi  13914  rngsubdir  13915  imasrng  13919  dfur2g  13925  srgass  13934  srgmulgass  13952  srgpcomp  13953  srglmhm  13956  srgrmhm  13957  crngcom  13977  ringass  13979  ringcom  13994  ringsubdi  14019  ringsubdir  14020  mulgass2  14021  ringlghm  14024  ringrghm  14025  imasring  14027  opprrng  14040  opprring  14042  oppr0g  14044  oppr1g  14045  opprnegg  14046  mulgass3  14048  dvdsrvald  14057  unitlinv  14090  unitrinv  14091  dvrfvald  14097  dvrass  14103  dvrdir  14107  rdivmuldivd  14108  rngidpropdg  14110  dvdsrpropdg  14111  unitpropdg  14112  invrpropdg  14113  rhm1  14131  rhmopp  14140  subrguss  14200  subrginv  14201  subrgdv  14202  lmodcom  14297  lmodsubdir  14309  rmodislmod  14315  lsppropd  14396  srascag  14406  sravscag  14407  ixpsnbasval  14430  rsp0  14457  lidlrsppropdg  14459  rnglidlmsgrp  14461  gsumfzfsumlemm  14551  expghmap  14571  mulgghm2  14572  mulgrhm  14573  zlmlemg  14592  zlmsca  14596  znle  14601  psrbasg  14638  psrplusgg  14642  psrlinv  14648  tgdom  14746  txbasval  14941  cnmpt11  14957  cnmpt21  14965  setsmsbasg  15153  bdbl  15177  dvmulxxbr  15376  dvimulf  15380  dvcj  15383  dvfre  15384  dvrecap  15387  dvmptc  15391  dvmptfsum  15399  dvef  15401  plyaddlem1  15421  plyrecj  15437  dvply1  15439  sinperlem  15482  coshalfpip  15496  ptolemy  15498  tangtx  15512  relogef  15538  rpcxpadd  15579  rpmulcxp  15583  rpdivcxp  15585  cxpmul  15586  rpcxpmul2  15587  abscxp  15589  rpcxpsqrt  15596  rpabscxpbnd  15614  rplogbreexp  15627  rprelogbmul  15629  rprelogbdiv  15631  1sgmprm  15668  perfect1  15672  perfectlem2  15674  perfect  15675  lgsneg  15703  lgsmod  15705  lgsdir2  15712  lgsdirprm  15713  lgsdir  15714  lgsdi  15716  lgssq  15719  lgssq2  15720  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem6  15746  lgseisenlem1  15749  lgseisenlem3  15751  lgseisenlem4  15752  lgsquadlem1  15756  lgsquad2  15762  2sqlem3  15796  setsiedg  15853  bj-charfundcALT  16172  nninfsellemeqinf  16382  refeq  16396