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 ⊢ (𝜑 → 𝐶 = 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  fnsnfv  5765  fvco2  5777  resfunexg  5939  fcof1  5992  fliftfun  6005  caovdir2d  6269  caov32d  6273  caov31d  6275  caov4d  6277  caovlem2d  6285  f1o3d  6301  caofcom  6337  caofdig  6340  cnvf1olem  6464  tfrlem1  6584  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  frecrdg  6684  oav2  6741  omv2  6743  omsuc  6750  nnmsucr  6766  ecovicom  6922  ecoviass  6924  ecovidi  6926  nnnninfeq  7474  nninfwlpoimlemg  7521  carden2bex  7541  addcompig  7702  addasspig  7703  mulcompig  7704  mulasspig  7705  distrpig  7706  addassnqg  7755  addnq0mo  7820  mulnq0mo  7821  nqnq0a  7827  nqnq0m  7828  distrnq0  7832  mulcomnq0  7833  addassnq0  7835  addcmpblnr  8112  mulcmpblnrlemg  8113  addsrmo  8116  mulsrmo  8117  ltsrprg  8120  recexgt0sr  8146  mulgt0sr  8151  mulextsr1lem  8153  addcnsrec  8215  mulcnsrec  8216  pitonnlem2  8220  recidpirqlemcalc  8230  axaddcom  8243  adddir  8323  mul32  8463  mul31  8464  add32  8492  add4  8494  sub32  8567  sub4  8578  subdir  8720  mulneg2  8730  mulreim  8940  apadd1  8944  apneg  8947  divassap  9028  divdirap  9035  divmul13ap  9053  divmul24ap  9054  divdiv32ap  9058  conjmulap  9067  zeo  9761  xaddcom  10279  xnegdi  10286  xaddass  10287  xaddass2  10288  xpncan  10289  xadd4d  10303  lincmb01cmp  10421  iccf1o  10423  flhalf  10757  modqvalp1  10800  modqdi  10849  modqsubdir  10850  frecuzrdgg  10873  seq3shft2  10938  seqshft2g  10939  seq3caopr3  10948  seqcaopr3g  10949  seq3caopr  10952  seqcaoprg  10953  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seqf1oglem2a  10975  seqf1oglem2  10977  seqf1og  10978  seq3homo  10984  seqfeq3  10986  seqhomog  10987  seqfeq4g  10988  seq3distr  10989  expp1  11003  expnegap0  11004  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  sqneg  11055  sqdivap  11060  subsq2  11104  binom2  11108  modqexp  11124  facp1  11189  bcm1k  11219  bcp1n  11220  bcval5  11222  omgadd  11263  hashun  11266  hashxp  11288  hashfibclem  11303  hashf1  11308  csbwrdg  11355  ccatass  11397  lswccatn0lsw  11400  swrdlsw  11462  swrdswrd  11498  wrd2ind  11516  swrdccatin1  11518  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatpfx1  11529  swrdccat3blem  11532  cats1catd  11561  shftfibg  11606  shftfib  11609  shftval  11611  2shfti  11617  seq3shft  11624  crre  11643  remim  11646  mulreap  11650  reneg  11654  readd  11655  remullem  11657  redivap  11660  imneg  11662  imadd  11663  imdivap  11667  cjcj  11669  cjadd  11670  cjmulrcl  11673  cjneg  11676  imval2  11680  resqrexlemcalc1  11801  absneg  11837  sqabsadd  11842  sqabssub  11843  absmul  11856  absresq  11866  absexp  11867  absexpzap  11868  bdtrilem  12029  xrmaxiflemcom  12039  xrmaxadd  12051  xrminrecl  12063  xrminadd  12065  serf0  12142  summodclem3  12171  fsum3  12178  isumss  12182  fisumss  12183  fsumadd  12197  isummulc1  12218  isumdivapc  12219  fsum2dlemstep  12225  fisumcom2  12229  fisum0diag2  12238  fsummulc2  12239  fsummulc1  12240  fsumdivapc  12241  fsumconst  12245  telfsumo  12257  fsumparts  12261  binomlem  12274  isumshft  12281  arisum2  12290  geolim  12302  geo2sum  12305  geo2lim  12307  cvgratnnlemseq  12317  cvgratz  12323  mertenslem2  12327  prodfrecap  12337  prodfdivap  12338  prodmodclem2a  12367  fprodntrivap  12375  fprodssdc  12381  fprodmul  12382  fprodabs  12407  fprod2dlemstep  12413  fprodcom2fi  12417  fprodrec  12420  efcllemp  12449  efcj  12464  efexp  12473  resinval  12506  recosval  12507  cosneg  12518  efival  12523  sinadd  12527  cosadd  12528  addcos  12537  sin2t  12540  cos2t  12541  dvdsmodexp  12586  odd2np1lem  12663  oexpneg  12668  neggcd  12784  gcdabs2  12791  mulgcd  12817  mulgcdr  12819  gcddiv  12820  rplpwr  12828  eucalgval  12856  eucalginv  12858  eucalg  12861  neglcm  12877  lcmgcd  12880  mulgcddvds  12896  qredeu  12899  nn0gcdsq  13004  phimullem  13031  prmdiv  13041  coprimeprodsq  13064  pythagtriplem1  13072  pythagtriplem3  13074  pythagtriplem4  13075  pythagtriplem12  13082  pceulem  13101  pceu  13102  pcqmul  13110  pcexp  13116  pcneg  13132  pcadd  13147  pcmpt  13150  pcmpt2  13151  pcbc  13158  4sqlem7  13191  4sqlem10  13194  mul4sqlem  13200  4sqlem11  13208  ballotfilemfp1  13288  ballotfilemieq  13317  ballotfilemgun  13325  ballotfilemfrc  13327  ennnfonelemp1  13354  setsabsd  13448  setscom  13449  ressbasd  13479  strressid  13483  ressinbasd  13486  ressressg  13487  ressplusgd  13541  imasival  13685  qusin  13705  fvprif  13722  xpsfeq  13724  grpidpropdg  13752  gzsumress  13770  mnd32g  13798  mnd4g  13800  imasmnd2  13817  0mhm  13851  resmhm  13852  mhmco  13855  gzsumwmhm  13861  grpinvcnv  13931  grpinvpropdg  13938  grpinvsub  13945  grpaddsubass  13953  grpsubpropdg  13967  grpsubpropd2  13968  imasgrp2  13971  imasgrp  13972  qusgrp2  13974  mulgnnp1  13991  mulgnegnn  13993  mulgaddcom  14007  mulginvcom  14008  mulgnndir  14012  mulgnn0ass  14019  mhmmulg  14024  mulgpropdg  14025  submmulg  14027  subginv  14042  subgsub  14047  subgmulg  14049  eqglact  14086  ghmsub  14112  ghmmulg  14117  resghm  14121  ghmeql  14128  conjghm  14137  ablsub4  14206  ablsub32  14215  imasabl  14229  gzsumreidx  14230  gzsumconst  14232  gzsumshift  14238  gsumvalfi  14241  gsumf1ofi  14249  gsummptfidmadd  14250  gsummptfidmsplitres  14254  gsumsplitfi  14255  gsumresfi  14262  gsummhmfi  14263  gsumconstcmn  14265  gsumressfi  14266  prdsval  14279  prdssgrpd  14297  prdsidlem  14299  prdsmndd  14300  prdsinvlem  14302  pwsplusgval  14314  pwsmulrval  14315  pws0g  14319  pwsinvg  14321  pwssub  14322  mgpress  14336  rngsubdi  14356  rngsubdir  14357  imasrng  14361  dfur2g  14372  srgass  14381  srgmulgass  14399  srgpcomp  14400  srglmhm  14403  srgrmhm  14404  crngcom  14424  ringass  14426  ringcom  14442  ringsubdi  14467  ringsubdir  14468  mulgass2  14469  ringlghm  14472  ringrghm  14473  imasring  14477  opprrng  14490  opprring  14492  oppr0g  14495  oppr1g  14496  opprnegg  14497  mulgass3  14499  dvdsrvald  14508  unitlinv  14541  unitrinv  14542  dvrfvald  14548  dvrass  14554  dvrdir  14558  rdivmuldivd  14559  rngidpropdg  14561  dvdsrpropdg  14562  unitpropdg  14563  invrpropdg  14564  rhm1  14582  rhmopp  14591  subrguss  14652  subrginv  14653  subrgdv  14654  rrgsupp  14682  aprprop  14709  opprdrng  14728  lmodcom  14778  lmodsubdir  14790  rmodislmod  14796  lsppropd  14877  srascag  14887  sravscag  14888  ixpsnbasval  14911  rsp0  14938  lidlrsppropdg  14940  rnglidlmsgrp  14942  gsumfsum  15031  expghmap  15050  mulgghm2  15051  mulgrhm  15052  zlmlemg  15071  zlmsca  15075  znle  15080  asclghm  15133  ascldimul  15139  assamulgscmlem1  15149  psrass1filem  15186  psrbasg  15187  psrplusgg  15191  psrlinv  15203  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  tgdom  15315  txbasval  15510  cnmpt11  15526  cnmpt21  15534  setsmsbasg  15722  bdbl  15746  dvmulxxbr  15945  dvimulf  15949  dvcj  15952  dvfre  15953  dvrecap  15956  dvmptc  15960  dvmptfsum  15968  dvef  15970  plyaddlem1  15990  plyrecj  16006  dvply1  16008  sinperlem  16052  coshalfpip  16066  ptolemy  16068  tangtx  16082  relogef  16110  logfac  16143  rpcxpadd  16155  rpmulcxp  16159  rpdivcxp  16161  cxpmul  16162  rpcxpmul2  16163  rpcxpmul2z  16165  abscxp  16167  rpcxpsqrt  16174  rpabscxpbnd  16192  rplogbreexp  16206  rprelogbmul  16208  rprelogbdiv  16210  birthdaylem2  16243  pellexlem3  16248  chtqfl  16275  ppiprm  16276  ppinprm  16277  chtnprm  16279  prmorcht  16299  1sgmprm  16305  perfect1  16315  perfectlem2  16317  perfect  16318  bcmono  16321  bposlem9  16336  lgsneg  16365  lgsmod  16367  lgsdir2  16374  lgsdirprm  16375  lgsdir  16376  lgsdi  16378  lgssq  16381  lgssq2  16382  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem6  16408  lgseisenlem1  16411  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlem1  16418  lgsquad2  16424  2sqlem3  16458  setsiedg  16515  vtxdeqd  16759  vtxdfifiun  16760  trlsegvdegfi  16930  depindlem3  16971  bj-charfundcALT  17057  nninfsellemeqinf  17282  refeq  17296