Theorem 3eqtr4d 2247

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	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4d	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4d

Step	Hyp	Ref	Expression
1		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
3		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr4d 2240	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
5	1, 4	eqtr4d 2240	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  fnsnfv  5637  fvco2  5647  resfunexg  5804  fcof1  5851  fliftfun  5864  caovdir2d  6122  caov32d  6126  caov31d  6128  caov4d  6130  caovlem2d  6138  caofcom  6188  caofdig  6191  cnvf1olem  6309  tfrlem1  6393  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  frecrdg  6493  oav2  6548  omv2  6550  omsuc  6557  nnmsucr  6573  ecovicom  6729  ecoviass  6731  ecovidi  6733  nnnninfeq  7229  nninfwlpoimlemg  7276  carden2bex  7296  addcompig  7441  addasspig  7442  mulcompig  7443  mulasspig  7444  distrpig  7445  addassnqg  7494  addnq0mo  7559  mulnq0mo  7560  nqnq0a  7566  nqnq0m  7567  distrnq0  7571  mulcomnq0  7572  addassnq0  7574  addcmpblnr  7851  mulcmpblnrlemg  7852  addsrmo  7855  mulsrmo  7856  ltsrprg  7859  recexgt0sr  7885  mulgt0sr  7890  mulextsr1lem  7892  addcnsrec  7954  mulcnsrec  7955  pitonnlem2  7959  recidpirqlemcalc  7969  axaddcom  7982  adddir  8062  mul32  8201  mul31  8202  add32  8230  add4  8232  sub32  8305  sub4  8316  subdir  8457  mulneg2  8467  mulreim  8676  apadd1  8680  apneg  8683  divassap  8762  divdirap  8769  divmul13ap  8787  divmul24ap  8788  divdiv32ap  8792  conjmulap  8801  zeo  9477  xaddcom  9982  xnegdi  9989  xaddass  9990  xaddass2  9991  xpncan  9992  xadd4d  10006  lincmb01cmp  10124  iccf1o  10125  flhalf  10443  modqvalp1  10486  modqdi  10535  modqsubdir  10536  frecuzrdgg  10559  seq3shft2  10624  seqshft2g  10625  seq3caopr3  10634  seqcaopr3g  10635  seq3caopr  10638  seqcaoprg  10639  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  seqf1oglem2a  10661  seqf1oglem2  10663  seqf1og  10664  seq3homo  10670  seqfeq3  10672  seqhomog  10673  seqfeq4g  10674  seq3distr  10675  expp1  10689  expnegap0  10690  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  sqneg  10741  sqdivap  10746  subsq2  10790  binom2  10794  modqexp  10809  facp1  10873  bcm1k  10903  bcp1n  10904  bcval5  10906  omgadd  10945  hashun  10948  hashxp  10969  csbwrdg  11021  ccatass  11062  lswccatn0lsw  11065  shftfibg  11073  shftfib  11076  shftval  11078  2shfti  11084  seq3shft  11091  crre  11110  remim  11113  mulreap  11117  reneg  11121  readd  11122  remullem  11124  redivap  11127  imneg  11129  imadd  11130  imdivap  11134  cjcj  11136  cjadd  11137  cjmulrcl  11140  cjneg  11143  imval2  11147  resqrexlemcalc1  11267  absneg  11303  sqabsadd  11308  sqabssub  11309  absmul  11322  absresq  11331  absexp  11332  absexpzap  11333  bdtrilem  11492  xrmaxiflemcom  11502  xrmaxadd  11514  xrminrecl  11526  xrminadd  11528  serf0  11605  summodclem3  11633  fsum3  11640  isumss  11644  fisumss  11645  fsumadd  11659  isummulc1  11680  isumdivapc  11681  fsum2dlemstep  11687  fisumcom2  11691  fisum0diag2  11700  fsummulc2  11701  fsummulc1  11702  fsumdivapc  11703  fsumconst  11707  telfsumo  11719  fsumparts  11723  binomlem  11736  isumshft  11743  arisum2  11752  geolim  11764  geo2sum  11767  geo2lim  11769  cvgratnnlemseq  11779  cvgratz  11785  mertenslem2  11789  prodfrecap  11799  prodfdivap  11800  prodmodclem2a  11829  fprodntrivap  11837  fprodssdc  11843  fprodmul  11844  fprodabs  11869  fprod2dlemstep  11875  fprodcom2fi  11879  fprodrec  11882  efcllemp  11911  efcj  11926  efexp  11935  resinval  11968  recosval  11969  cosneg  11980  efival  11985  sinadd  11989  cosadd  11990  addcos  11999  sin2t  12002  cos2t  12003  dvdsmodexp  12048  odd2np1lem  12125  oexpneg  12130  neggcd  12246  gcdabs2  12253  mulgcd  12279  mulgcdr  12281  gcddiv  12282  rplpwr  12290  eucalgval  12318  eucalginv  12320  eucalg  12323  neglcm  12339  lcmgcd  12342  mulgcddvds  12358  qredeu  12361  nn0gcdsq  12464  phimullem  12489  prmdiv  12499  coprimeprodsq  12522  pythagtriplem1  12530  pythagtriplem3  12532  pythagtriplem4  12533  pythagtriplem12  12540  pceulem  12559  pceu  12560  pcqmul  12568  pcexp  12574  pcneg  12590  pcadd  12605  pcmpt  12608  pcmpt2  12609  pcbc  12616  4sqlem7  12649  4sqlem10  12652  mul4sqlem  12658  4sqlem11  12666  ennnfonelemp1  12719  setsabsd  12813  setscom  12814  ressbasd  12841  strressid  12845  ressinbasd  12848  ressressg  12849  ressplusgd  12903  prdsval  13047  pwsplusgval  13069  pwsmulrval  13070  imasival  13080  qusin  13100  fvprif  13117  xpsfeq  13119  grpidpropdg  13148  gsumpropd  13166  gsumpropd2  13167  gsumress  13169  prdssgrpd  13189  mnd32g  13201  mnd4g  13203  prdsidlem  13221  prdsmndd  13222  pws0g  13225  imasmnd2  13226  0mhm  13260  resmhm  13261  mhmco  13264  gsumwmhm  13272  grpinvcnv  13342  grpinvpropdg  13349  grpinvsub  13356  grpaddsubass  13364  grpsubpropdg  13378  grpsubpropd2  13379  prdsinvlem  13382  pwsinvg  13386  pwssub  13387  imasgrp2  13388  imasgrp  13389  qusgrp2  13391  mulgnnp1  13408  mulgnegnn  13410  mulgaddcom  13424  mulginvcom  13425  mulgnndir  13429  mulgnn0ass  13436  mhmmulg  13441  mulgpropdg  13442  submmulg  13444  subginv  13459  subgsub  13464  subgmulg  13466  eqglact  13503  ghmsub  13529  ghmmulg  13534  resghm  13538  ghmeql  13545  conjghm  13554  ablsub4  13591  ablsub32  13600  imasabl  13614  gsumfzreidx  13615  gsumfzmptfidmadd  13617  gsumfzconst  13619  mgpress  13635  rngsubdi  13655  rngsubdir  13656  imasrng  13660  dfur2g  13666  srgass  13675  srgmulgass  13693  srgpcomp  13694  srglmhm  13697  srgrmhm  13698  crngcom  13718  ringass  13720  ringcom  13735  ringsubdi  13760  ringsubdir  13761  mulgass2  13762  ringlghm  13765  ringrghm  13766  imasring  13768  opprrng  13781  opprring  13783  oppr0g  13785  oppr1g  13786  opprnegg  13787  mulgass3  13789  dvdsrvald  13797  unitlinv  13830  unitrinv  13831  dvrfvald  13837  dvrass  13843  dvrdir  13847  rdivmuldivd  13848  rngidpropdg  13850  dvdsrpropdg  13851  unitpropdg  13852  invrpropdg  13853  rhm1  13871  rhmopp  13880  subrguss  13940  subrginv  13941  subrgdv  13942  lmodcom  14037  lmodsubdir  14049  rmodislmod  14055  lsppropd  14136  srascag  14146  sravscag  14147  ixpsnbasval  14170  rsp0  14197  lidlrsppropdg  14199  rnglidlmsgrp  14201  gsumfzfsumlemm  14291  expghmap  14311  mulgghm2  14312  mulgrhm  14313  zlmlemg  14332  zlmsca  14336  znle  14341  psrbasg  14378  psrplusgg  14382  psrlinv  14388  tgdom  14486  txbasval  14681  cnmpt11  14697  cnmpt21  14705  setsmsbasg  14893  bdbl  14917  dvmulxxbr  15116  dvimulf  15120  dvcj  15123  dvfre  15124  dvrecap  15127  dvmptc  15131  dvmptfsum  15139  dvef  15141  plyaddlem1  15161  plyrecj  15177  dvply1  15179  sinperlem  15222  coshalfpip  15236  ptolemy  15238  tangtx  15252  relogef  15278  rpcxpadd  15319  rpmulcxp  15323  rpdivcxp  15325  cxpmul  15326  rpcxpmul2  15327  abscxp  15329  rpcxpsqrt  15336  rpabscxpbnd  15354  rplogbreexp  15367  rprelogbmul  15369  rprelogbdiv  15371  1sgmprm  15408  perfect1  15412  perfectlem2  15414  perfect  15415  lgsneg  15443  lgsmod  15445  lgsdir2  15452  lgsdirprm  15453  lgsdir  15454  lgsdi  15456  lgssq  15459  lgssq2  15460  lgsdirnn0  15466  lgsdinn0  15467  gausslemma2dlem6  15486  lgseisenlem1  15489  lgseisenlem3  15491  lgseisenlem4  15492  lgsquadlem1  15496  lgsquad2  15502  2sqlem3  15536  bj-charfundcALT  15678  nninfsellemeqinf  15886  refeq  15900