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  5638  fvco2  5648  resfunexg  5805  fcof1  5852  fliftfun  5865  caovdir2d  6123  caov32d  6127  caov31d  6129  caov4d  6131  caovlem2d  6139  caofcom  6189  caofdig  6192  cnvf1olem  6310  tfrlem1  6394  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  frecrdg  6494  oav2  6549  omv2  6551  omsuc  6558  nnmsucr  6574  ecovicom  6730  ecoviass  6732  ecovidi  6734  nnnninfeq  7230  nninfwlpoimlemg  7277  carden2bex  7297  addcompig  7442  addasspig  7443  mulcompig  7444  mulasspig  7445  distrpig  7446  addassnqg  7495  addnq0mo  7560  mulnq0mo  7561  nqnq0a  7567  nqnq0m  7568  distrnq0  7572  mulcomnq0  7573  addassnq0  7575  addcmpblnr  7852  mulcmpblnrlemg  7853  addsrmo  7856  mulsrmo  7857  ltsrprg  7860  recexgt0sr  7886  mulgt0sr  7891  mulextsr1lem  7893  addcnsrec  7955  mulcnsrec  7956  pitonnlem2  7960  recidpirqlemcalc  7970  axaddcom  7983  adddir  8063  mul32  8202  mul31  8203  add32  8231  add4  8233  sub32  8306  sub4  8317  subdir  8458  mulneg2  8468  mulreim  8677  apadd1  8681  apneg  8684  divassap  8763  divdirap  8770  divmul13ap  8788  divmul24ap  8789  divdiv32ap  8793  conjmulap  8802  zeo  9478  xaddcom  9983  xnegdi  9990  xaddass  9991  xaddass2  9992  xpncan  9993  xadd4d  10007  lincmb01cmp  10125  iccf1o  10126  flhalf  10445  modqvalp1  10488  modqdi  10537  modqsubdir  10538  frecuzrdgg  10561  seq3shft2  10626  seqshft2g  10627  seq3caopr3  10636  seqcaopr3g  10637  seq3caopr  10640  seqcaoprg  10641  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seqf1oglem2a  10663  seqf1oglem2  10665  seqf1og  10666  seq3homo  10672  seqfeq3  10674  seqhomog  10675  seqfeq4g  10676  seq3distr  10677  expp1  10691  expnegap0  10692  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  sqneg  10743  sqdivap  10748  subsq2  10792  binom2  10796  modqexp  10811  facp1  10875  bcm1k  10905  bcp1n  10906  bcval5  10908  omgadd  10947  hashun  10950  hashxp  10971  csbwrdg  11023  ccatass  11064  lswccatn0lsw  11067  swrdlsw  11122  shftfibg  11131  shftfib  11134  shftval  11136  2shfti  11142  seq3shft  11149  crre  11168  remim  11171  mulreap  11175  reneg  11179  readd  11180  remullem  11182  redivap  11185  imneg  11187  imadd  11188  imdivap  11192  cjcj  11194  cjadd  11195  cjmulrcl  11198  cjneg  11201  imval2  11205  resqrexlemcalc1  11325  absneg  11361  sqabsadd  11366  sqabssub  11367  absmul  11380  absresq  11389  absexp  11390  absexpzap  11391  bdtrilem  11550  xrmaxiflemcom  11560  xrmaxadd  11572  xrminrecl  11584  xrminadd  11586  serf0  11663  summodclem3  11691  fsum3  11698  isumss  11702  fisumss  11703  fsumadd  11717  isummulc1  11738  isumdivapc  11739  fsum2dlemstep  11745  fisumcom2  11749  fisum0diag2  11758  fsummulc2  11759  fsummulc1  11760  fsumdivapc  11761  fsumconst  11765  telfsumo  11777  fsumparts  11781  binomlem  11794  isumshft  11801  arisum2  11810  geolim  11822  geo2sum  11825  geo2lim  11827  cvgratnnlemseq  11837  cvgratz  11843  mertenslem2  11847  prodfrecap  11857  prodfdivap  11858  prodmodclem2a  11887  fprodntrivap  11895  fprodssdc  11901  fprodmul  11902  fprodabs  11927  fprod2dlemstep  11933  fprodcom2fi  11937  fprodrec  11940  efcllemp  11969  efcj  11984  efexp  11993  resinval  12026  recosval  12027  cosneg  12038  efival  12043  sinadd  12047  cosadd  12048  addcos  12057  sin2t  12060  cos2t  12061  dvdsmodexp  12106  odd2np1lem  12183  oexpneg  12188  neggcd  12304  gcdabs2  12311  mulgcd  12337  mulgcdr  12339  gcddiv  12340  rplpwr  12348  eucalgval  12376  eucalginv  12378  eucalg  12381  neglcm  12397  lcmgcd  12400  mulgcddvds  12416  qredeu  12419  nn0gcdsq  12522  phimullem  12547  prmdiv  12557  coprimeprodsq  12580  pythagtriplem1  12588  pythagtriplem3  12590  pythagtriplem4  12591  pythagtriplem12  12598  pceulem  12617  pceu  12618  pcqmul  12626  pcexp  12632  pcneg  12648  pcadd  12663  pcmpt  12666  pcmpt2  12667  pcbc  12674  4sqlem7  12707  4sqlem10  12710  mul4sqlem  12716  4sqlem11  12724  ennnfonelemp1  12777  setsabsd  12871  setscom  12872  ressbasd  12899  strressid  12903  ressinbasd  12906  ressressg  12907  ressplusgd  12961  prdsval  13105  pwsplusgval  13127  pwsmulrval  13128  imasival  13138  qusin  13158  fvprif  13175  xpsfeq  13177  grpidpropdg  13206  gsumpropd  13224  gsumpropd2  13225  gsumress  13227  prdssgrpd  13247  mnd32g  13259  mnd4g  13261  prdsidlem  13279  prdsmndd  13280  pws0g  13283  imasmnd2  13284  0mhm  13318  resmhm  13319  mhmco  13322  gsumwmhm  13330  grpinvcnv  13400  grpinvpropdg  13407  grpinvsub  13414  grpaddsubass  13422  grpsubpropdg  13436  grpsubpropd2  13437  prdsinvlem  13440  pwsinvg  13444  pwssub  13445  imasgrp2  13446  imasgrp  13447  qusgrp2  13449  mulgnnp1  13466  mulgnegnn  13468  mulgaddcom  13482  mulginvcom  13483  mulgnndir  13487  mulgnn0ass  13494  mhmmulg  13499  mulgpropdg  13500  submmulg  13502  subginv  13517  subgsub  13522  subgmulg  13524  eqglact  13561  ghmsub  13587  ghmmulg  13592  resghm  13596  ghmeql  13603  conjghm  13612  ablsub4  13649  ablsub32  13658  imasabl  13672  gsumfzreidx  13673  gsumfzmptfidmadd  13675  gsumfzconst  13677  mgpress  13693  rngsubdi  13713  rngsubdir  13714  imasrng  13718  dfur2g  13724  srgass  13733  srgmulgass  13751  srgpcomp  13752  srglmhm  13755  srgrmhm  13756  crngcom  13776  ringass  13778  ringcom  13793  ringsubdi  13818  ringsubdir  13819  mulgass2  13820  ringlghm  13823  ringrghm  13824  imasring  13826  opprrng  13839  opprring  13841  oppr0g  13843  oppr1g  13844  opprnegg  13845  mulgass3  13847  dvdsrvald  13855  unitlinv  13888  unitrinv  13889  dvrfvald  13895  dvrass  13901  dvrdir  13905  rdivmuldivd  13906  rngidpropdg  13908  dvdsrpropdg  13909  unitpropdg  13910  invrpropdg  13911  rhm1  13929  rhmopp  13938  subrguss  13998  subrginv  13999  subrgdv  14000  lmodcom  14095  lmodsubdir  14107  rmodislmod  14113  lsppropd  14194  srascag  14204  sravscag  14205  ixpsnbasval  14228  rsp0  14255  lidlrsppropdg  14257  rnglidlmsgrp  14259  gsumfzfsumlemm  14349  expghmap  14369  mulgghm2  14370  mulgrhm  14371  zlmlemg  14390  zlmsca  14394  znle  14399  psrbasg  14436  psrplusgg  14440  psrlinv  14446  tgdom  14544  txbasval  14739  cnmpt11  14755  cnmpt21  14763  setsmsbasg  14951  bdbl  14975  dvmulxxbr  15174  dvimulf  15178  dvcj  15181  dvfre  15182  dvrecap  15185  dvmptc  15189  dvmptfsum  15197  dvef  15199  plyaddlem1  15219  plyrecj  15235  dvply1  15237  sinperlem  15280  coshalfpip  15294  ptolemy  15296  tangtx  15310  relogef  15336  rpcxpadd  15377  rpmulcxp  15381  rpdivcxp  15383  cxpmul  15384  rpcxpmul2  15385  abscxp  15387  rpcxpsqrt  15394  rpabscxpbnd  15412  rplogbreexp  15425  rprelogbmul  15427  rprelogbdiv  15429  1sgmprm  15466  perfect1  15470  perfectlem2  15472  perfect  15473  lgsneg  15501  lgsmod  15503  lgsdir2  15510  lgsdirprm  15511  lgsdir  15512  lgsdi  15514  lgssq  15517  lgssq2  15518  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem6  15544  lgseisenlem1  15547  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlem1  15554  lgsquad2  15560  2sqlem3  15594  bj-charfundcALT  15745  nninfsellemeqinf  15953  refeq  15967