Theorem 3eqtr4d 2274

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  fnsnfv  5714  fvco2  5724  resfunexg  5883  fcof1  5934  fliftfun  5947  caovdir2d  6209  caov32d  6213  caov31d  6215  caov4d  6217  caovlem2d  6225  caofcom  6275  caofdig  6278  cnvf1olem  6398  tfrlem1  6517  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  frecrdg  6617  oav2  6674  omv2  6676  omsuc  6683  nnmsucr  6699  ecovicom  6855  ecoviass  6857  ecovidi  6859  nnnninfeq  7370  nninfwlpoimlemg  7417  carden2bex  7437  addcompig  7592  addasspig  7593  mulcompig  7594  mulasspig  7595  distrpig  7596  addassnqg  7645  addnq0mo  7710  mulnq0mo  7711  nqnq0a  7717  nqnq0m  7718  distrnq0  7722  mulcomnq0  7723  addassnq0  7725  addcmpblnr  8002  mulcmpblnrlemg  8003  addsrmo  8006  mulsrmo  8007  ltsrprg  8010  recexgt0sr  8036  mulgt0sr  8041  mulextsr1lem  8043  addcnsrec  8105  mulcnsrec  8106  pitonnlem2  8110  recidpirqlemcalc  8120  axaddcom  8133  adddir  8213  mul32  8352  mul31  8353  add32  8381  add4  8383  sub32  8456  sub4  8467  subdir  8608  mulneg2  8618  mulreim  8827  apadd1  8831  apneg  8834  divassap  8913  divdirap  8920  divmul13ap  8938  divmul24ap  8939  divdiv32ap  8943  conjmulap  8952  zeo  9628  xaddcom  10139  xnegdi  10146  xaddass  10147  xaddass2  10148  xpncan  10149  xadd4d  10163  lincmb01cmp  10281  iccf1o  10282  flhalf  10606  modqvalp1  10649  modqdi  10698  modqsubdir  10699  frecuzrdgg  10722  seq3shft2  10787  seqshft2g  10788  seq3caopr3  10797  seqcaopr3g  10798  seq3caopr  10801  seqcaoprg  10802  seq3f1olemqsumkj  10817  seq3f1olemqsumk  10818  seq3f1olemqsum  10819  seqf1oglem2a  10824  seqf1oglem2  10826  seqf1og  10827  seq3homo  10833  seqfeq3  10835  seqhomog  10836  seqfeq4g  10837  seq3distr  10838  expp1  10852  expnegap0  10853  expaddzaplem  10888  expaddzap  10889  expmulzap  10891  sqneg  10904  sqdivap  10909  subsq2  10953  binom2  10957  modqexp  10972  facp1  11036  bcm1k  11066  bcp1n  11067  bcval5  11069  omgadd  11109  hashun  11112  hashxp  11134  csbwrdg  11190  ccatass  11232  lswccatn0lsw  11235  swrdlsw  11297  swrdswrd  11333  wrd2ind  11351  swrdccatin1  11353  swrdccatin2  11357  pfxccatin12lem2  11359  pfxccatin12lem3  11360  pfxccatpfx1  11364  swrdccat3blem  11367  cats1catd  11396  shftfibg  11441  shftfib  11444  shftval  11446  2shfti  11452  seq3shft  11459  crre  11478  remim  11481  mulreap  11485  reneg  11489  readd  11490  remullem  11492  redivap  11495  imneg  11497  imadd  11498  imdivap  11502  cjcj  11504  cjadd  11505  cjmulrcl  11508  cjneg  11511  imval2  11515  resqrexlemcalc1  11635  absneg  11671  sqabsadd  11676  sqabssub  11677  absmul  11690  absresq  11699  absexp  11700  absexpzap  11701  bdtrilem  11860  xrmaxiflemcom  11870  xrmaxadd  11882  xrminrecl  11894  xrminadd  11896  serf0  11973  summodclem3  12002  fsum3  12009  isumss  12013  fisumss  12014  fsumadd  12028  isummulc1  12049  isumdivapc  12050  fsum2dlemstep  12056  fisumcom2  12060  fisum0diag2  12069  fsummulc2  12070  fsummulc1  12071  fsumdivapc  12072  fsumconst  12076  telfsumo  12088  fsumparts  12092  binomlem  12105  isumshft  12112  arisum2  12121  geolim  12133  geo2sum  12136  geo2lim  12138  cvgratnnlemseq  12148  cvgratz  12154  mertenslem2  12158  prodfrecap  12168  prodfdivap  12169  prodmodclem2a  12198  fprodntrivap  12206  fprodssdc  12212  fprodmul  12213  fprodabs  12238  fprod2dlemstep  12244  fprodcom2fi  12248  fprodrec  12251  efcllemp  12280  efcj  12295  efexp  12304  resinval  12337  recosval  12338  cosneg  12349  efival  12354  sinadd  12358  cosadd  12359  addcos  12368  sin2t  12371  cos2t  12372  dvdsmodexp  12417  odd2np1lem  12494  oexpneg  12499  neggcd  12615  gcdabs2  12622  mulgcd  12648  mulgcdr  12650  gcddiv  12651  rplpwr  12659  eucalgval  12687  eucalginv  12689  eucalg  12692  neglcm  12708  lcmgcd  12711  mulgcddvds  12727  qredeu  12730  nn0gcdsq  12833  phimullem  12858  prmdiv  12868  coprimeprodsq  12891  pythagtriplem1  12899  pythagtriplem3  12901  pythagtriplem4  12902  pythagtriplem12  12909  pceulem  12928  pceu  12929  pcqmul  12937  pcexp  12943  pcneg  12959  pcadd  12974  pcmpt  12977  pcmpt2  12978  pcbc  12985  4sqlem7  13018  4sqlem10  13021  mul4sqlem  13027  4sqlem11  13035  ennnfonelemp1  13088  setsabsd  13182  setscom  13183  ressbasd  13211  strressid  13215  ressinbasd  13218  ressressg  13219  ressplusgd  13273  prdsval  13417  pwsplusgval  13439  pwsmulrval  13440  imasival  13450  qusin  13470  fvprif  13487  xpsfeq  13489  grpidpropdg  13518  gsumpropd  13536  gsumpropd2  13537  gsumress  13539  prdssgrpd  13559  mnd32g  13571  mnd4g  13573  prdsidlem  13591  prdsmndd  13592  pws0g  13595  imasmnd2  13596  0mhm  13630  resmhm  13631  mhmco  13634  gsumwmhm  13642  grpinvcnv  13712  grpinvpropdg  13719  grpinvsub  13726  grpaddsubass  13734  grpsubpropdg  13748  grpsubpropd2  13749  prdsinvlem  13752  pwsinvg  13756  pwssub  13757  imasgrp2  13758  imasgrp  13759  qusgrp2  13761  mulgnnp1  13778  mulgnegnn  13780  mulgaddcom  13794  mulginvcom  13795  mulgnndir  13799  mulgnn0ass  13806  mhmmulg  13811  mulgpropdg  13812  submmulg  13814  subginv  13829  subgsub  13834  subgmulg  13836  eqglact  13873  ghmsub  13899  ghmmulg  13904  resghm  13908  ghmeql  13915  conjghm  13924  ablsub4  13961  ablsub32  13970  imasabl  13984  gsumfzreidx  13985  gsumfzmptfidmadd  13987  gsumfzconst  13989  mgpress  14006  rngsubdi  14026  rngsubdir  14027  imasrng  14031  dfur2g  14037  srgass  14046  srgmulgass  14064  srgpcomp  14065  srglmhm  14068  srgrmhm  14069  crngcom  14089  ringass  14091  ringcom  14106  ringsubdi  14131  ringsubdir  14132  mulgass2  14133  ringlghm  14136  ringrghm  14137  imasring  14139  opprrng  14152  opprring  14154  oppr0g  14156  oppr1g  14157  opprnegg  14158  mulgass3  14160  dvdsrvald  14169  unitlinv  14202  unitrinv  14203  dvrfvald  14209  dvrass  14215  dvrdir  14219  rdivmuldivd  14220  rngidpropdg  14222  dvdsrpropdg  14223  unitpropdg  14224  invrpropdg  14225  rhm1  14243  rhmopp  14252  subrguss  14312  subrginv  14313  subrgdv  14314  lmodcom  14409  lmodsubdir  14421  rmodislmod  14427  lsppropd  14508  srascag  14518  sravscag  14519  ixpsnbasval  14542  rsp0  14569  lidlrsppropdg  14571  rnglidlmsgrp  14573  gsumfzfsumlemm  14663  expghmap  14683  mulgghm2  14684  mulgrhm  14685  zlmlemg  14704  zlmsca  14708  znle  14713  psrbasg  14755  psrplusgg  14759  psrlinv  14765  tgdom  14863  txbasval  15058  cnmpt11  15074  cnmpt21  15082  setsmsbasg  15270  bdbl  15294  dvmulxxbr  15493  dvimulf  15497  dvcj  15500  dvfre  15501  dvrecap  15504  dvmptc  15508  dvmptfsum  15516  dvef  15518  plyaddlem1  15538  plyrecj  15554  dvply1  15556  sinperlem  15599  coshalfpip  15613  ptolemy  15615  tangtx  15629  relogef  15655  rpcxpadd  15696  rpmulcxp  15700  rpdivcxp  15702  cxpmul  15703  rpcxpmul2  15704  abscxp  15706  rpcxpsqrt  15713  rpabscxpbnd  15731  rplogbreexp  15744  rprelogbmul  15746  rprelogbdiv  15748  1sgmprm  15785  perfect1  15789  perfectlem2  15791  perfect  15792  lgsneg  15820  lgsmod  15822  lgsdir2  15829  lgsdirprm  15830  lgsdir  15831  lgsdi  15833  lgssq  15836  lgssq2  15837  lgsdirnn0  15843  lgsdinn0  15844  gausslemma2dlem6  15863  lgseisenlem1  15866  lgseisenlem3  15868  lgseisenlem4  15869  lgsquadlem1  15873  lgsquad2  15879  2sqlem3  15913  setsiedg  15970  vtxdeqd  16214  vtxdfifiun  16215  trlsegvdegfi  16385  depindlem3  16426  bj-charfundcALT  16502  nninfsellemeqinf  16719  refeq  16733  gfsumval  16786  gsumgfsumlem  16789