Theorem 3eqtr4d 2239

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fnsnfv  5623  fvco2  5633  resfunexg  5786  fcof1  5833  fliftfun  5846  caovdir2d  6104  caov32d  6108  caov31d  6110  caov4d  6112  caovlem2d  6120  caofcom  6170  caofdig  6173  cnvf1olem  6291  tfrlem1  6375  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  frecrdg  6475  oav2  6530  omv2  6532  omsuc  6539  nnmsucr  6555  ecovicom  6711  ecoviass  6713  ecovidi  6715  nnnninfeq  7203  nninfwlpoimlemg  7250  carden2bex  7270  addcompig  7415  addasspig  7416  mulcompig  7417  mulasspig  7418  distrpig  7419  addassnqg  7468  addnq0mo  7533  mulnq0mo  7534  nqnq0a  7540  nqnq0m  7541  distrnq0  7545  mulcomnq0  7546  addassnq0  7548  addcmpblnr  7825  mulcmpblnrlemg  7826  addsrmo  7829  mulsrmo  7830  ltsrprg  7833  recexgt0sr  7859  mulgt0sr  7864  mulextsr1lem  7866  addcnsrec  7928  mulcnsrec  7929  pitonnlem2  7933  recidpirqlemcalc  7943  axaddcom  7956  adddir  8036  mul32  8175  mul31  8176  add32  8204  add4  8206  sub32  8279  sub4  8290  subdir  8431  mulneg2  8441  mulreim  8650  apadd1  8654  apneg  8657  divassap  8736  divdirap  8743  divmul13ap  8761  divmul24ap  8762  divdiv32ap  8766  conjmulap  8775  zeo  9450  xaddcom  9955  xnegdi  9962  xaddass  9963  xaddass2  9964  xpncan  9965  xadd4d  9979  lincmb01cmp  10097  iccf1o  10098  flhalf  10411  modqvalp1  10454  modqdi  10503  modqsubdir  10504  frecuzrdgg  10527  seq3shft2  10592  seqshft2g  10593  seq3caopr3  10602  seqcaopr3g  10603  seq3caopr  10606  seqcaoprg  10607  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seqf1oglem2a  10629  seqf1oglem2  10631  seqf1og  10632  seq3homo  10638  seqfeq3  10640  seqhomog  10641  seqfeq4g  10642  seq3distr  10643  expp1  10657  expnegap0  10658  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  sqneg  10709  sqdivap  10714  subsq2  10758  binom2  10762  modqexp  10777  facp1  10841  bcm1k  10871  bcp1n  10872  bcval5  10874  omgadd  10913  hashun  10916  hashxp  10937  csbwrdg  10983  shftfibg  11004  shftfib  11007  shftval  11009  2shfti  11015  seq3shft  11022  crre  11041  remim  11044  mulreap  11048  reneg  11052  readd  11053  remullem  11055  redivap  11058  imneg  11060  imadd  11061  imdivap  11065  cjcj  11067  cjadd  11068  cjmulrcl  11071  cjneg  11074  imval2  11078  resqrexlemcalc1  11198  absneg  11234  sqabsadd  11239  sqabssub  11240  absmul  11253  absresq  11262  absexp  11263  absexpzap  11264  bdtrilem  11423  xrmaxiflemcom  11433  xrmaxadd  11445  xrminrecl  11457  xrminadd  11459  serf0  11536  summodclem3  11564  fsum3  11571  isumss  11575  fisumss  11576  fsumadd  11590  isummulc1  11611  isumdivapc  11612  fsum2dlemstep  11618  fisumcom2  11622  fisum0diag2  11631  fsummulc2  11632  fsummulc1  11633  fsumdivapc  11634  fsumconst  11638  telfsumo  11650  fsumparts  11654  binomlem  11667  isumshft  11674  arisum2  11683  geolim  11695  geo2sum  11698  geo2lim  11700  cvgratnnlemseq  11710  cvgratz  11716  mertenslem2  11720  prodfrecap  11730  prodfdivap  11731  prodmodclem2a  11760  fprodntrivap  11768  fprodssdc  11774  fprodmul  11775  fprodabs  11800  fprod2dlemstep  11806  fprodcom2fi  11810  fprodrec  11813  efcllemp  11842  efcj  11857  efexp  11866  resinval  11899  recosval  11900  cosneg  11911  efival  11916  sinadd  11920  cosadd  11921  addcos  11930  sin2t  11933  cos2t  11934  dvdsmodexp  11979  odd2np1lem  12056  oexpneg  12061  neggcd  12177  gcdabs2  12184  mulgcd  12210  mulgcdr  12212  gcddiv  12213  rplpwr  12221  eucalgval  12249  eucalginv  12251  eucalg  12254  neglcm  12270  lcmgcd  12273  mulgcddvds  12289  qredeu  12292  nn0gcdsq  12395  phimullem  12420  prmdiv  12430  coprimeprodsq  12453  pythagtriplem1  12461  pythagtriplem3  12463  pythagtriplem4  12464  pythagtriplem12  12471  pceulem  12490  pceu  12491  pcqmul  12499  pcexp  12505  pcneg  12521  pcadd  12536  pcmpt  12539  pcmpt2  12540  pcbc  12547  4sqlem7  12580  4sqlem10  12583  mul4sqlem  12589  4sqlem11  12597  ennnfonelemp1  12650  setsabsd  12744  setscom  12745  ressbasd  12772  strressid  12776  ressinbasd  12779  ressressg  12780  ressplusgd  12833  prdsval  12977  pwsplusgval  12999  pwsmulrval  13000  imasival  13010  qusin  13030  fvprif  13047  xpsfeq  13049  grpidpropdg  13078  gsumpropd  13096  gsumpropd2  13097  gsumress  13099  prdssgrpd  13119  mnd32g  13131  mnd4g  13133  prdsidlem  13151  prdsmndd  13152  pws0g  13155  imasmnd2  13156  0mhm  13190  resmhm  13191  mhmco  13194  gsumwmhm  13202  grpinvcnv  13272  grpinvpropdg  13279  grpinvsub  13286  grpaddsubass  13294  grpsubpropdg  13308  grpsubpropd2  13309  prdsinvlem  13312  pwsinvg  13316  pwssub  13317  imasgrp2  13318  imasgrp  13319  qusgrp2  13321  mulgnnp1  13338  mulgnegnn  13340  mulgaddcom  13354  mulginvcom  13355  mulgnndir  13359  mulgnn0ass  13366  mhmmulg  13371  mulgpropdg  13372  submmulg  13374  subginv  13389  subgsub  13394  subgmulg  13396  eqglact  13433  ghmsub  13459  ghmmulg  13464  resghm  13468  ghmeql  13475  conjghm  13484  ablsub4  13521  ablsub32  13530  imasabl  13544  gsumfzreidx  13545  gsumfzmptfidmadd  13547  gsumfzconst  13549  mgpress  13565  rngsubdi  13585  rngsubdir  13586  imasrng  13590  dfur2g  13596  srgass  13605  srgmulgass  13623  srgpcomp  13624  srglmhm  13627  srgrmhm  13628  crngcom  13648  ringass  13650  ringcom  13665  ringsubdi  13690  ringsubdir  13691  mulgass2  13692  ringlghm  13695  ringrghm  13696  imasring  13698  opprrng  13711  opprring  13713  oppr0g  13715  oppr1g  13716  opprnegg  13717  mulgass3  13719  dvdsrvald  13727  unitlinv  13760  unitrinv  13761  dvrfvald  13767  dvrass  13773  dvrdir  13777  rdivmuldivd  13778  rngidpropdg  13780  dvdsrpropdg  13781  unitpropdg  13782  invrpropdg  13783  rhm1  13801  rhmopp  13810  subrguss  13870  subrginv  13871  subrgdv  13872  lmodcom  13967  lmodsubdir  13979  rmodislmod  13985  lsppropd  14066  srascag  14076  sravscag  14077  ixpsnbasval  14100  rsp0  14127  lidlrsppropdg  14129  rnglidlmsgrp  14131  gsumfzfsumlemm  14221  expghmap  14241  mulgghm2  14242  mulgrhm  14243  zlmlemg  14262  zlmsca  14266  znle  14271  psrbasg  14308  psrplusgg  14312  psrlinv  14318  tgdom  14416  txbasval  14611  cnmpt11  14627  cnmpt21  14635  setsmsbasg  14823  bdbl  14847  dvmulxxbr  15046  dvimulf  15050  dvcj  15053  dvfre  15054  dvrecap  15057  dvmptc  15061  dvmptfsum  15069  dvef  15071  plyaddlem1  15091  plyrecj  15107  dvply1  15109  sinperlem  15152  coshalfpip  15166  ptolemy  15168  tangtx  15182  relogef  15208  rpcxpadd  15249  rpmulcxp  15253  rpdivcxp  15255  cxpmul  15256  rpcxpmul2  15257  abscxp  15259  rpcxpsqrt  15266  rpabscxpbnd  15284  rplogbreexp  15297  rprelogbmul  15299  rprelogbdiv  15301  1sgmprm  15338  perfect1  15342  perfectlem2  15344  perfect  15345  lgsneg  15373  lgsmod  15375  lgsdir2  15382  lgsdirprm  15383  lgsdir  15384  lgsdi  15386  lgssq  15389  lgssq2  15390  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem6  15416  lgseisenlem1  15419  lgseisenlem3  15421  lgseisenlem4  15422  lgsquadlem1  15426  lgsquad2  15432  2sqlem3  15466  bj-charfundcALT  15563  nninfsellemeqinf  15771  refeq  15785