Theorem 3eqtr4d 2208

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

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  fnsnfv  5545  fvco2  5555  resfunexg  5706  fcof1  5751  fliftfun  5764  caovdir2d  6018  caov32d  6022  caov31d  6024  caov4d  6026  caovlem2d  6034  caofcom  6073  cnvf1olem  6192  tfrlem1  6276  tfrlemisucaccv  6293  tfr1onlemsucaccv  6309  tfrcllemsucaccv  6322  frecrdg  6376  oav2  6431  omv2  6433  omsuc  6440  nnmsucr  6456  ecovicom  6609  ecoviass  6611  ecovidi  6613  nnnninfeq  7092  carden2bex  7145  addcompig  7270  addasspig  7271  mulcompig  7272  mulasspig  7273  distrpig  7274  addassnqg  7323  addnq0mo  7388  mulnq0mo  7389  nqnq0a  7395  nqnq0m  7396  distrnq0  7400  mulcomnq0  7401  addassnq0  7403  addcmpblnr  7680  mulcmpblnrlemg  7681  addsrmo  7684  mulsrmo  7685  ltsrprg  7688  recexgt0sr  7714  mulgt0sr  7719  mulextsr1lem  7721  addcnsrec  7783  mulcnsrec  7784  pitonnlem2  7788  recidpirqlemcalc  7798  axaddcom  7811  adddir  7890  mul32  8028  mul31  8029  add32  8057  add4  8059  sub32  8132  sub4  8143  subdir  8284  mulneg2  8294  mulreim  8502  apadd1  8506  apneg  8509  divassap  8586  divdirap  8593  divmul13ap  8611  divmul24ap  8612  divdiv32ap  8616  conjmulap  8625  zeo  9296  xaddcom  9797  xnegdi  9804  xaddass  9805  xaddass2  9806  xpncan  9807  xadd4d  9821  lincmb01cmp  9939  iccf1o  9940  flhalf  10237  modqvalp1  10278  modqdi  10327  modqsubdir  10328  frecuzrdgg  10351  seq3shft2  10408  seq3caopr3  10416  seq3caopr  10418  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3homo  10445  seqfeq3  10447  seq3distr  10448  expp1  10462  expnegap0  10463  expaddzaplem  10498  expaddzap  10499  expmulzap  10501  sqneg  10514  sqdivap  10519  subsq2  10562  binom2  10566  modqexp  10581  facp1  10643  bcm1k  10673  bcp1n  10674  bcval5  10676  omgadd  10715  hashun  10718  hashxp  10739  shftfibg  10762  shftfib  10765  shftval  10767  2shfti  10773  seq3shft  10780  crre  10799  remim  10802  mulreap  10806  reneg  10810  readd  10811  remullem  10813  redivap  10816  imneg  10818  imadd  10819  imdivap  10823  cjcj  10825  cjadd  10826  cjmulrcl  10829  cjneg  10832  imval2  10836  resqrexlemcalc1  10956  absneg  10992  sqabsadd  10997  sqabssub  10998  absmul  11011  absresq  11020  absexp  11021  absexpzap  11022  bdtrilem  11180  xrmaxiflemcom  11190  xrmaxadd  11202  xrminrecl  11214  xrminadd  11216  serf0  11293  summodclem3  11321  fsum3  11328  isumss  11332  fisumss  11333  fsumadd  11347  isummulc1  11368  isumdivapc  11369  fsum2dlemstep  11375  fisumcom2  11379  fisum0diag2  11388  fsummulc2  11389  fsummulc1  11390  fsumdivapc  11391  fsumconst  11395  telfsumo  11407  fsumparts  11411  binomlem  11424  isumshft  11431  arisum2  11440  geolim  11452  geo2sum  11455  geo2lim  11457  cvgratnnlemseq  11467  cvgratz  11473  mertenslem2  11477  prodfrecap  11487  prodfdivap  11488  prodmodclem2a  11517  fprodntrivap  11525  fprodssdc  11531  fprodmul  11532  fprodabs  11557  fprod2dlemstep  11563  fprodcom2fi  11567  fprodrec  11570  efcllemp  11599  efcj  11614  efexp  11623  resinval  11656  recosval  11657  cosneg  11668  efival  11673  sinadd  11677  cosadd  11678  addcos  11687  sin2t  11690  cos2t  11691  dvdsmodexp  11735  odd2np1lem  11809  oexpneg  11814  neggcd  11916  gcdabs2  11923  mulgcd  11949  mulgcdr  11951  gcddiv  11952  rplpwr  11960  eucalgval  11986  eucalginv  11988  eucalg  11991  neglcm  12007  lcmgcd  12010  mulgcddvds  12026  qredeu  12029  nn0gcdsq  12132  phimullem  12157  prmdiv  12167  coprimeprodsq  12189  pythagtriplem1  12197  pythagtriplem3  12199  pythagtriplem4  12200  pythagtriplem12  12207  pceulem  12226  pceu  12227  pcqmul  12235  pcexp  12241  pcneg  12256  pcadd  12271  pcmpt  12273  pcmpt2  12274  pcbc  12281  4sqlem7  12314  4sqlem10  12317  mul4sqlem  12323  ennnfonelemp1  12339  setsabsd  12433  setscom  12434  grpidpropdg  12605  tgdom  12712  txbasval  12907  cnmpt11  12923  cnmpt21  12931  setsmsbasg  13119  bdbl  13143  dvmulxxbr  13306  dvimulf  13310  dvcj  13313  dvfre  13314  dvrecap  13317  dvef  13328  sinperlem  13369  coshalfpip  13383  ptolemy  13385  tangtx  13399  relogef  13425  rpcxpadd  13466  rpmulcxp  13470  rpdivcxp  13472  cxpmul  13473  abscxp  13475  rpcxpsqrt  13482  rpabscxpbnd  13499  rplogbreexp  13511  rprelogbmul  13513  rprelogbdiv  13515  lgsneg  13565  lgsmod  13567  lgsdir2  13574  lgsdirprm  13575  lgsdir  13576  lgsdi  13578  lgssq  13581  lgssq2  13582  lgsdirnn0  13588  lgsdinn0  13589  2sqlem3  13593  bj-charfundcALT  13691  nninfsellemeqinf  13896  refeq  13907