Theorem 3eqtr4d 2281

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 2274	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
5	1, 4	eqtr4d 2274	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  fnsnfv  5756  fvco2  5768  resfunexg  5927  fcof1  5979  fliftfun  5992  caovdir2d  6256  caov32d  6260  caov31d  6262  caov4d  6264  caovlem2d  6272  f1o3d  6288  caofcom  6323  caofdig  6326  cnvf1olem  6450  tfrlem1  6569  tfrlemisucaccv  6586  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  frecrdg  6669  oav2  6726  omv2  6728  omsuc  6735  nnmsucr  6751  ecovicom  6907  ecoviass  6909  ecovidi  6911  nnnninfeq  7458  nninfwlpoimlemg  7505  carden2bex  7525  addcompig  7686  addasspig  7687  mulcompig  7688  mulasspig  7689  distrpig  7690  addassnqg  7739  addnq0mo  7804  mulnq0mo  7805  nqnq0a  7811  nqnq0m  7812  distrnq0  7816  mulcomnq0  7817  addassnq0  7819  addcmpblnr  8096  mulcmpblnrlemg  8097  addsrmo  8100  mulsrmo  8101  ltsrprg  8104  recexgt0sr  8130  mulgt0sr  8135  mulextsr1lem  8137  addcnsrec  8199  mulcnsrec  8200  pitonnlem2  8204  recidpirqlemcalc  8214  axaddcom  8227  adddir  8307  mul32  8446  mul31  8447  add32  8475  add4  8477  sub32  8550  sub4  8561  subdir  8703  mulneg2  8713  mulreim  8922  apadd1  8926  apneg  8929  divassap  9010  divdirap  9017  divmul13ap  9035  divmul24ap  9036  divdiv32ap  9040  conjmulap  9049  zeo  9730  xaddcom  10242  xnegdi  10249  xaddass  10250  xaddass2  10251  xpncan  10252  xadd4d  10266  lincmb01cmp  10384  iccf1o  10386  flhalf  10715  modqvalp1  10758  modqdi  10807  modqsubdir  10808  frecuzrdgg  10831  seq3shft2  10896  seqshft2g  10897  seq3caopr3  10906  seqcaopr3g  10907  seq3caopr  10910  seqcaoprg  10911  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seqf1oglem2a  10933  seqf1oglem2  10935  seqf1og  10936  seq3homo  10942  seqfeq3  10944  seqhomog  10945  seqfeq4g  10946  seq3distr  10947  expp1  10961  expnegap0  10962  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  sqneg  11013  sqdivap  11018  subsq2  11062  binom2  11066  modqexp  11082  facp1  11146  bcm1k  11176  bcp1n  11177  bcval5  11179  omgadd  11220  hashun  11223  hashxp  11245  hashfibclem  11260  hashf1  11265  csbwrdg  11312  ccatass  11354  lswccatn0lsw  11357  swrdlsw  11419  swrdswrd  11455  wrd2ind  11473  swrdccatin1  11475  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccatpfx1  11486  swrdccat3blem  11489  cats1catd  11518  shftfibg  11563  shftfib  11566  shftval  11568  2shfti  11574  seq3shft  11581  crre  11600  remim  11603  mulreap  11607  reneg  11611  readd  11612  remullem  11614  redivap  11617  imneg  11619  imadd  11620  imdivap  11624  cjcj  11626  cjadd  11627  cjmulrcl  11630  cjneg  11633  imval2  11637  resqrexlemcalc1  11758  absneg  11794  sqabsadd  11799  sqabssub  11800  absmul  11813  absresq  11822  absexp  11823  absexpzap  11824  bdtrilem  11983  xrmaxiflemcom  11993  xrmaxadd  12005  xrminrecl  12017  xrminadd  12019  serf0  12096  summodclem3  12125  fsum3  12132  isumss  12136  fisumss  12137  fsumadd  12151  isummulc1  12172  isumdivapc  12173  fsum2dlemstep  12179  fisumcom2  12183  fisum0diag2  12192  fsummulc2  12193  fsummulc1  12194  fsumdivapc  12195  fsumconst  12199  telfsumo  12211  fsumparts  12215  binomlem  12228  isumshft  12235  arisum2  12244  geolim  12256  geo2sum  12259  geo2lim  12261  cvgratnnlemseq  12271  cvgratz  12277  mertenslem2  12281  prodfrecap  12291  prodfdivap  12292  prodmodclem2a  12321  fprodntrivap  12329  fprodssdc  12335  fprodmul  12336  fprodabs  12361  fprod2dlemstep  12367  fprodcom2fi  12371  fprodrec  12374  efcllemp  12403  efcj  12418  efexp  12427  resinval  12460  recosval  12461  cosneg  12472  efival  12477  sinadd  12481  cosadd  12482  addcos  12491  sin2t  12494  cos2t  12495  dvdsmodexp  12540  odd2np1lem  12617  oexpneg  12622  neggcd  12738  gcdabs2  12745  mulgcd  12771  mulgcdr  12773  gcddiv  12774  rplpwr  12782  eucalgval  12810  eucalginv  12812  eucalg  12815  neglcm  12831  lcmgcd  12834  mulgcddvds  12850  qredeu  12853  nn0gcdsq  12956  phimullem  12981  prmdiv  12991  coprimeprodsq  13014  pythagtriplem1  13022  pythagtriplem3  13024  pythagtriplem4  13025  pythagtriplem12  13032  pceulem  13051  pceu  13052  pcqmul  13060  pcexp  13066  pcneg  13082  pcadd  13097  pcmpt  13100  pcmpt2  13101  pcbc  13108  4sqlem7  13141  4sqlem10  13144  mul4sqlem  13150  4sqlem11  13158  ballotfilemfp1  13209  ballotfilemieq  13238  ballotfilemgun  13246  ballotfilemfrc  13248  ennnfonelemp1  13275  setsabsd  13369  setscom  13370  ressbasd  13398  strressid  13402  ressinbasd  13405  ressressg  13406  ressplusgd  13460  imasival  13604  qusin  13624  fvprif  13641  xpsfeq  13643  grpidpropdg  13671  gzsumress  13689  mnd32g  13717  mnd4g  13719  imasmnd2  13736  0mhm  13770  resmhm  13771  mhmco  13774  gzsumwmhm  13780  grpinvcnv  13850  grpinvpropdg  13857  grpinvsub  13864  grpaddsubass  13872  grpsubpropdg  13886  grpsubpropd2  13887  imasgrp2  13890  imasgrp  13891  qusgrp2  13893  mulgnnp1  13910  mulgnegnn  13912  mulgaddcom  13926  mulginvcom  13927  mulgnndir  13931  mulgnn0ass  13938  mhmmulg  13943  mulgpropdg  13944  submmulg  13946  subginv  13961  subgsub  13966  subgmulg  13968  eqglact  14005  ghmsub  14031  ghmmulg  14036  resghm  14040  ghmeql  14047  conjghm  14056  ablsub4  14094  ablsub32  14103  imasabl  14117  gzsumreidx  14118  gzsumconst  14120  gzsumshift  14126  gsumvalfi  14129  gsumf1ofi  14137  gsummptfidmadd  14138  gsummhmfi  14141  gsumconstcmn  14143  gsumressfi  14144  prdsval  14150  prdssgrpd  14168  prdsidlem  14170  prdsmndd  14171  prdsinvlem  14173  pwsplusgval  14185  pwsmulrval  14186  pws0g  14190  pwsinvg  14192  pwssub  14193  mgpress  14205  rngsubdi  14225  rngsubdir  14226  imasrng  14230  dfur2g  14240  srgass  14249  srgmulgass  14267  srgpcomp  14268  srglmhm  14271  srgrmhm  14272  crngcom  14292  ringass  14294  ringcom  14309  ringsubdi  14334  ringsubdir  14335  mulgass2  14336  ringlghm  14339  ringrghm  14340  imasring  14342  opprrng  14355  opprring  14357  oppr0g  14360  oppr1g  14361  opprnegg  14362  mulgass3  14364  dvdsrvald  14373  unitlinv  14406  unitrinv  14407  dvrfvald  14413  dvrass  14419  dvrdir  14423  rdivmuldivd  14424  rngidpropdg  14426  dvdsrpropdg  14427  unitpropdg  14428  invrpropdg  14429  rhm1  14447  rhmopp  14456  subrguss  14517  subrginv  14518  subrgdv  14519  rrgsupp  14547  aprprop  14574  opprdrng  14593  lmodcom  14642  lmodsubdir  14654  rmodislmod  14660  lsppropd  14741  srascag  14751  sravscag  14752  ixpsnbasval  14775  rsp0  14802  lidlrsppropdg  14804  rnglidlmsgrp  14806  gsumfsum  14895  expghmap  14914  mulgghm2  14915  mulgrhm  14916  zlmlemg  14935  zlmsca  14939  znle  14944  psrbasg  14988  psrplusgg  14992  psrlinv  14998  tgdom  15096  txbasval  15291  cnmpt11  15307  cnmpt21  15315  setsmsbasg  15503  bdbl  15527  dvmulxxbr  15726  dvimulf  15730  dvcj  15733  dvfre  15734  dvrecap  15737  dvmptc  15741  dvmptfsum  15749  dvef  15751  plyaddlem1  15771  plyrecj  15787  dvply1  15789  sinperlem  15832  coshalfpip  15846  ptolemy  15848  tangtx  15862  relogef  15888  logfac  15918  rpcxpadd  15930  rpmulcxp  15934  rpdivcxp  15936  cxpmul  15937  rpcxpmul2  15938  abscxp  15940  rpcxpsqrt  15947  rpabscxpbnd  15965  rplogbreexp  15978  rprelogbmul  15980  rprelogbdiv  15982  pellexlem3  16007  1sgmprm  16022  perfect1  16026  perfectlem2  16028  perfect  16029  lgsneg  16057  lgsmod  16059  lgsdir2  16066  lgsdirprm  16067  lgsdir  16068  lgsdi  16070  lgssq  16073  lgssq2  16074  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem6  16100  lgseisenlem1  16103  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlem1  16110  lgsquad2  16116  2sqlem3  16150  setsiedg  16207  vtxdeqd  16451  vtxdfifiun  16452  trlsegvdegfi  16622  depindlem3  16663  bj-charfundcALT  16749  nninfsellemeqinf  16964  refeq  16978