Theorem 3eqtr4d 2182

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  fnsnfv  5480  fvco2  5490  resfunexg  5641  fcof1  5684  fliftfun  5697  caovdir2d  5947  caov32d  5951  caov31d  5953  caov4d  5955  caovlem2d  5963  caofcom  6005  cnvf1olem  6121  tfrlem1  6205  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  frecrdg  6305  oav2  6359  omv2  6361  omsuc  6368  nnmsucr  6384  ecovicom  6537  ecoviass  6539  ecovidi  6541  carden2bex  7045  addcompig  7137  addasspig  7138  mulcompig  7139  mulasspig  7140  distrpig  7141  addassnqg  7190  addnq0mo  7255  mulnq0mo  7256  nqnq0a  7262  nqnq0m  7263  distrnq0  7267  mulcomnq0  7268  addassnq0  7270  addcmpblnr  7547  mulcmpblnrlemg  7548  addsrmo  7551  mulsrmo  7552  ltsrprg  7555  recexgt0sr  7581  mulgt0sr  7586  mulextsr1lem  7588  addcnsrec  7650  mulcnsrec  7651  pitonnlem2  7655  recidpirqlemcalc  7665  axaddcom  7678  adddir  7757  mul32  7892  mul31  7893  add32  7921  add4  7923  sub32  7996  sub4  8007  subdir  8148  mulneg2  8158  mulreim  8366  apadd1  8370  apneg  8373  divassap  8450  divdirap  8457  divmul13ap  8475  divmul24ap  8476  divdiv32ap  8480  conjmulap  8489  zeo  9156  xaddcom  9644  xnegdi  9651  xaddass  9652  xaddass2  9653  xpncan  9654  xadd4d  9668  lincmb01cmp  9786  iccf1o  9787  flhalf  10075  modqvalp1  10116  modqdi  10165  modqsubdir  10166  frecuzrdgg  10189  seq3shft2  10246  seq3caopr3  10254  seq3caopr  10256  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3homo  10283  seqfeq3  10285  seq3distr  10286  expp1  10300  expnegap0  10301  expaddzaplem  10336  expaddzap  10337  expmulzap  10339  sqneg  10352  sqdivap  10357  subsq2  10400  binom2  10403  facp1  10476  bcm1k  10506  bcp1n  10507  bcval5  10509  omgadd  10548  hashun  10551  hashxp  10572  shftfibg  10592  shftfib  10595  shftval  10597  2shfti  10603  seq3shft  10610  crre  10629  remim  10632  mulreap  10636  reneg  10640  readd  10641  remullem  10643  redivap  10646  imneg  10648  imadd  10649  imdivap  10653  cjcj  10655  cjadd  10656  cjmulrcl  10659  cjneg  10662  imval2  10666  resqrexlemcalc1  10786  absneg  10822  sqabsadd  10827  sqabssub  10828  absmul  10841  absresq  10850  absexp  10851  absexpzap  10852  bdtrilem  11010  xrmaxiflemcom  11018  xrmaxadd  11030  xrminrecl  11042  xrminadd  11044  serf0  11121  summodclem3  11149  fsum3  11156  isumss  11160  fisumss  11161  fsumadd  11175  isummulc1  11196  isumdivapc  11197  fsum2dlemstep  11203  fisumcom2  11207  fisum0diag2  11216  fsummulc2  11217  fsummulc1  11218  fsumdivapc  11219  fsumconst  11223  telfsumo  11235  fsumparts  11239  binomlem  11252  isumshft  11259  arisum2  11268  geolim  11280  geo2sum  11283  geo2lim  11285  cvgratnnlemseq  11295  cvgratz  11301  mertenslem2  11305  prodfrecap  11315  prodfdivap  11316  prodmodclem2a  11345  efcllemp  11364  efcj  11379  efexp  11388  resinval  11422  recosval  11423  cosneg  11434  efival  11439  sinadd  11443  cosadd  11444  addcos  11453  sin2t  11456  cos2t  11457  odd2np1lem  11569  oexpneg  11574  neggcd  11671  gcdabs2  11678  mulgcd  11704  mulgcdr  11706  gcddiv  11707  rplpwr  11715  eucalgval  11735  eucalginv  11737  eucalg  11740  neglcm  11756  lcmgcd  11759  mulgcddvds  11775  qredeu  11778  nn0gcdsq  11878  phimullem  11901  ennnfonelemp1  11919  setsabsd  11998  setscom  11999  tgdom  12241  txbasval  12436  cnmpt11  12452  cnmpt21  12460  setsmsbasg  12648  bdbl  12672  dvmulxxbr  12835  dvimulf  12839  dvcj  12842  dvfre  12843  dvrecap  12846  dvef  12856  sinperlem  12889  coshalfpip  12903  ptolemy  12905  tangtx  12919  nninfalllemn  13202  nninfsellemeqinf  13212  refeq  13223