Theorem 3eqtr4d 2250

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 2243	. 2 |- ( ph -> D = A )
5	1, 4	eqtr4d 2243	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  fnsnfv  5661  fvco2  5671  resfunexg  5828  fcof1  5875  fliftfun  5888  caovdir2d  6146  caov32d  6150  caov31d  6152  caov4d  6154  caovlem2d  6162  caofcom  6212  caofdig  6215  cnvf1olem  6333  tfrlem1  6417  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  frecrdg  6517  oav2  6572  omv2  6574  omsuc  6581  nnmsucr  6597  ecovicom  6753  ecoviass  6755  ecovidi  6757  nnnninfeq  7256  nninfwlpoimlemg  7303  carden2bex  7323  addcompig  7477  addasspig  7478  mulcompig  7479  mulasspig  7480  distrpig  7481  addassnqg  7530  addnq0mo  7595  mulnq0mo  7596  nqnq0a  7602  nqnq0m  7603  distrnq0  7607  mulcomnq0  7608  addassnq0  7610  addcmpblnr  7887  mulcmpblnrlemg  7888  addsrmo  7891  mulsrmo  7892  ltsrprg  7895  recexgt0sr  7921  mulgt0sr  7926  mulextsr1lem  7928  addcnsrec  7990  mulcnsrec  7991  pitonnlem2  7995  recidpirqlemcalc  8005  axaddcom  8018  adddir  8098  mul32  8237  mul31  8238  add32  8266  add4  8268  sub32  8341  sub4  8352  subdir  8493  mulneg2  8503  mulreim  8712  apadd1  8716  apneg  8719  divassap  8798  divdirap  8805  divmul13ap  8823  divmul24ap  8824  divdiv32ap  8828  conjmulap  8837  zeo  9513  xaddcom  10018  xnegdi  10025  xaddass  10026  xaddass2  10027  xpncan  10028  xadd4d  10042  lincmb01cmp  10160  iccf1o  10161  flhalf  10482  modqvalp1  10525  modqdi  10574  modqsubdir  10575  frecuzrdgg  10598  seq3shft2  10663  seqshft2g  10664  seq3caopr3  10673  seqcaopr3g  10674  seq3caopr  10677  seqcaoprg  10678  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seqf1oglem2a  10700  seqf1oglem2  10702  seqf1og  10703  seq3homo  10709  seqfeq3  10711  seqhomog  10712  seqfeq4g  10713  seq3distr  10714  expp1  10728  expnegap0  10729  expaddzaplem  10764  expaddzap  10765  expmulzap  10767  sqneg  10780  sqdivap  10785  subsq2  10829  binom2  10833  modqexp  10848  facp1  10912  bcm1k  10942  bcp1n  10943  bcval5  10945  omgadd  10984  hashun  10987  hashxp  11008  csbwrdg  11060  ccatass  11102  lswccatn0lsw  11105  swrdlsw  11160  swrdswrd  11196  wrd2ind  11214  swrdccatin1  11216  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccatpfx1  11227  swrdccat3blem  11230  shftfibg  11246  shftfib  11249  shftval  11251  2shfti  11257  seq3shft  11264  crre  11283  remim  11286  mulreap  11290  reneg  11294  readd  11295  remullem  11297  redivap  11300  imneg  11302  imadd  11303  imdivap  11307  cjcj  11309  cjadd  11310  cjmulrcl  11313  cjneg  11316  imval2  11320  resqrexlemcalc1  11440  absneg  11476  sqabsadd  11481  sqabssub  11482  absmul  11495  absresq  11504  absexp  11505  absexpzap  11506  bdtrilem  11665  xrmaxiflemcom  11675  xrmaxadd  11687  xrminrecl  11699  xrminadd  11701  serf0  11778  summodclem3  11806  fsum3  11813  isumss  11817  fisumss  11818  fsumadd  11832  isummulc1  11853  isumdivapc  11854  fsum2dlemstep  11860  fisumcom2  11864  fisum0diag2  11873  fsummulc2  11874  fsummulc1  11875  fsumdivapc  11876  fsumconst  11880  telfsumo  11892  fsumparts  11896  binomlem  11909  isumshft  11916  arisum2  11925  geolim  11937  geo2sum  11940  geo2lim  11942  cvgratnnlemseq  11952  cvgratz  11958  mertenslem2  11962  prodfrecap  11972  prodfdivap  11973  prodmodclem2a  12002  fprodntrivap  12010  fprodssdc  12016  fprodmul  12017  fprodabs  12042  fprod2dlemstep  12048  fprodcom2fi  12052  fprodrec  12055  efcllemp  12084  efcj  12099  efexp  12108  resinval  12141  recosval  12142  cosneg  12153  efival  12158  sinadd  12162  cosadd  12163  addcos  12172  sin2t  12175  cos2t  12176  dvdsmodexp  12221  odd2np1lem  12298  oexpneg  12303  neggcd  12419  gcdabs2  12426  mulgcd  12452  mulgcdr  12454  gcddiv  12455  rplpwr  12463  eucalgval  12491  eucalginv  12493  eucalg  12496  neglcm  12512  lcmgcd  12515  mulgcddvds  12531  qredeu  12534  nn0gcdsq  12637  phimullem  12662  prmdiv  12672  coprimeprodsq  12695  pythagtriplem1  12703  pythagtriplem3  12705  pythagtriplem4  12706  pythagtriplem12  12713  pceulem  12732  pceu  12733  pcqmul  12741  pcexp  12747  pcneg  12763  pcadd  12778  pcmpt  12781  pcmpt2  12782  pcbc  12789  4sqlem7  12822  4sqlem10  12825  mul4sqlem  12831  4sqlem11  12839  ennnfonelemp1  12892  setsabsd  12986  setscom  12987  ressbasd  13014  strressid  13018  ressinbasd  13021  ressressg  13022  ressplusgd  13076  prdsval  13220  pwsplusgval  13242  pwsmulrval  13243  imasival  13253  qusin  13273  fvprif  13290  xpsfeq  13292  grpidpropdg  13321  gsumpropd  13339  gsumpropd2  13340  gsumress  13342  prdssgrpd  13362  mnd32g  13374  mnd4g  13376  prdsidlem  13394  prdsmndd  13395  pws0g  13398  imasmnd2  13399  0mhm  13433  resmhm  13434  mhmco  13437  gsumwmhm  13445  grpinvcnv  13515  grpinvpropdg  13522  grpinvsub  13529  grpaddsubass  13537  grpsubpropdg  13551  grpsubpropd2  13552  prdsinvlem  13555  pwsinvg  13559  pwssub  13560  imasgrp2  13561  imasgrp  13562  qusgrp2  13564  mulgnnp1  13581  mulgnegnn  13583  mulgaddcom  13597  mulginvcom  13598  mulgnndir  13602  mulgnn0ass  13609  mhmmulg  13614  mulgpropdg  13615  submmulg  13617  subginv  13632  subgsub  13637  subgmulg  13639  eqglact  13676  ghmsub  13702  ghmmulg  13707  resghm  13711  ghmeql  13718  conjghm  13727  ablsub4  13764  ablsub32  13773  imasabl  13787  gsumfzreidx  13788  gsumfzmptfidmadd  13790  gsumfzconst  13792  mgpress  13808  rngsubdi  13828  rngsubdir  13829  imasrng  13833  dfur2g  13839  srgass  13848  srgmulgass  13866  srgpcomp  13867  srglmhm  13870  srgrmhm  13871  crngcom  13891  ringass  13893  ringcom  13908  ringsubdi  13933  ringsubdir  13934  mulgass2  13935  ringlghm  13938  ringrghm  13939  imasring  13941  opprrng  13954  opprring  13956  oppr0g  13958  oppr1g  13959  opprnegg  13960  mulgass3  13962  dvdsrvald  13970  unitlinv  14003  unitrinv  14004  dvrfvald  14010  dvrass  14016  dvrdir  14020  rdivmuldivd  14021  rngidpropdg  14023  dvdsrpropdg  14024  unitpropdg  14025  invrpropdg  14026  rhm1  14044  rhmopp  14053  subrguss  14113  subrginv  14114  subrgdv  14115  lmodcom  14210  lmodsubdir  14222  rmodislmod  14228  lsppropd  14309  srascag  14319  sravscag  14320  ixpsnbasval  14343  rsp0  14370  lidlrsppropdg  14372  rnglidlmsgrp  14374  gsumfzfsumlemm  14464  expghmap  14484  mulgghm2  14485  mulgrhm  14486  zlmlemg  14505  zlmsca  14509  znle  14514  psrbasg  14551  psrplusgg  14555  psrlinv  14561  tgdom  14659  txbasval  14854  cnmpt11  14870  cnmpt21  14878  setsmsbasg  15066  bdbl  15090  dvmulxxbr  15289  dvimulf  15293  dvcj  15296  dvfre  15297  dvrecap  15300  dvmptc  15304  dvmptfsum  15312  dvef  15314  plyaddlem1  15334  plyrecj  15350  dvply1  15352  sinperlem  15395  coshalfpip  15409  ptolemy  15411  tangtx  15425  relogef  15451  rpcxpadd  15492  rpmulcxp  15496  rpdivcxp  15498  cxpmul  15499  rpcxpmul2  15500  abscxp  15502  rpcxpsqrt  15509  rpabscxpbnd  15527  rplogbreexp  15540  rprelogbmul  15542  rprelogbdiv  15544  1sgmprm  15581  perfect1  15585  perfectlem2  15587  perfect  15588  lgsneg  15616  lgsmod  15618  lgsdir2  15625  lgsdirprm  15626  lgsdir  15627  lgsdi  15629  lgssq  15632  lgssq2  15633  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem6  15659  lgseisenlem1  15662  lgseisenlem3  15664  lgseisenlem4  15665  lgsquadlem1  15669  lgsquad2  15675  2sqlem3  15709  bj-charfundcALT  15944  nninfsellemeqinf  16155  refeq  16169