Theorem 3eqtr4d 2232

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 2225	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
5	1, 4	eqtr4d 2225	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  fnsnfv  5603  fvco2  5613  resfunexg  5765  fcof1  5812  fliftfun  5825  caovdir2d  6081  caov32d  6085  caov31d  6087  caov4d  6089  caovlem2d  6097  caofcom  6138  cnvf1olem  6257  tfrlem1  6341  tfrlemisucaccv  6358  tfr1onlemsucaccv  6374  tfrcllemsucaccv  6387  frecrdg  6441  oav2  6496  omv2  6498  omsuc  6505  nnmsucr  6521  ecovicom  6677  ecoviass  6679  ecovidi  6681  nnnninfeq  7166  nninfwlpoimlemg  7213  carden2bex  7228  addcompig  7368  addasspig  7369  mulcompig  7370  mulasspig  7371  distrpig  7372  addassnqg  7421  addnq0mo  7486  mulnq0mo  7487  nqnq0a  7493  nqnq0m  7494  distrnq0  7498  mulcomnq0  7499  addassnq0  7501  addcmpblnr  7778  mulcmpblnrlemg  7779  addsrmo  7782  mulsrmo  7783  ltsrprg  7786  recexgt0sr  7812  mulgt0sr  7817  mulextsr1lem  7819  addcnsrec  7881  mulcnsrec  7882  pitonnlem2  7886  recidpirqlemcalc  7896  axaddcom  7909  adddir  7989  mul32  8128  mul31  8129  add32  8157  add4  8159  sub32  8232  sub4  8243  subdir  8384  mulneg2  8394  mulreim  8602  apadd1  8606  apneg  8609  divassap  8688  divdirap  8695  divmul13ap  8713  divmul24ap  8714  divdiv32ap  8718  conjmulap  8727  zeo  9399  xaddcom  9903  xnegdi  9910  xaddass  9911  xaddass2  9912  xpncan  9913  xadd4d  9927  lincmb01cmp  10045  iccf1o  10046  flhalf  10345  modqvalp1  10386  modqdi  10435  modqsubdir  10436  frecuzrdgg  10459  seq3shft2  10518  seq3caopr3  10526  seq3caopr  10528  seq3f1olemqsumkj  10543  seq3f1olemqsumk  10544  seq3f1olemqsum  10545  seq3homo  10555  seqfeq3  10557  seqfeq4g  10558  seq3distr  10559  expp1  10573  expnegap0  10574  expaddzaplem  10609  expaddzap  10610  expmulzap  10612  sqneg  10625  sqdivap  10630  subsq2  10674  binom2  10678  modqexp  10693  facp1  10757  bcm1k  10787  bcp1n  10788  bcval5  10790  omgadd  10829  hashun  10832  hashxp  10853  shftfibg  10876  shftfib  10879  shftval  10881  2shfti  10887  seq3shft  10894  crre  10913  remim  10916  mulreap  10920  reneg  10924  readd  10925  remullem  10927  redivap  10930  imneg  10932  imadd  10933  imdivap  10937  cjcj  10939  cjadd  10940  cjmulrcl  10943  cjneg  10946  imval2  10950  resqrexlemcalc1  11070  absneg  11106  sqabsadd  11111  sqabssub  11112  absmul  11125  absresq  11134  absexp  11135  absexpzap  11136  bdtrilem  11294  xrmaxiflemcom  11304  xrmaxadd  11316  xrminrecl  11328  xrminadd  11330  serf0  11407  summodclem3  11435  fsum3  11442  isumss  11446  fisumss  11447  fsumadd  11461  isummulc1  11482  isumdivapc  11483  fsum2dlemstep  11489  fisumcom2  11493  fisum0diag2  11502  fsummulc2  11503  fsummulc1  11504  fsumdivapc  11505  fsumconst  11509  telfsumo  11521  fsumparts  11525  binomlem  11538  isumshft  11545  arisum2  11554  geolim  11566  geo2sum  11569  geo2lim  11571  cvgratnnlemseq  11581  cvgratz  11587  mertenslem2  11591  prodfrecap  11601  prodfdivap  11602  prodmodclem2a  11631  fprodntrivap  11639  fprodssdc  11645  fprodmul  11646  fprodabs  11671  fprod2dlemstep  11677  fprodcom2fi  11681  fprodrec  11684  efcllemp  11713  efcj  11728  efexp  11737  resinval  11770  recosval  11771  cosneg  11782  efival  11787  sinadd  11791  cosadd  11792  addcos  11801  sin2t  11804  cos2t  11805  dvdsmodexp  11849  odd2np1lem  11924  oexpneg  11929  neggcd  12031  gcdabs2  12038  mulgcd  12064  mulgcdr  12066  gcddiv  12067  rplpwr  12075  eucalgval  12103  eucalginv  12105  eucalg  12108  neglcm  12124  lcmgcd  12127  mulgcddvds  12143  qredeu  12146  nn0gcdsq  12249  phimullem  12274  prmdiv  12284  coprimeprodsq  12306  pythagtriplem1  12314  pythagtriplem3  12316  pythagtriplem4  12317  pythagtriplem12  12324  pceulem  12343  pceu  12344  pcqmul  12352  pcexp  12358  pcneg  12374  pcadd  12389  pcmpt  12392  pcmpt2  12393  pcbc  12400  4sqlem7  12433  4sqlem10  12436  mul4sqlem  12442  4sqlem11  12450  ennnfonelemp1  12474  setsabsd  12568  setscom  12569  ressbasd  12596  strressid  12600  ressinbasd  12603  ressressg  12604  ressplusgd  12657  imasival  12800  qusin  12820  fvprif  12837  xpsfeq  12839  grpidpropdg  12868  gsumpropd  12885  gsumpropd2  12886  gsumress  12888  mnd32g  12918  mnd4g  12920  0mhm  12968  resmhm  12969  mhmco  12972  grpinvcnv  13043  grpinvpropdg  13050  grpinvsub  13057  grpaddsubass  13065  grpsubpropdg  13079  grpsubpropd2  13080  imasgrp2  13083  imasgrp  13084  qusgrp2  13086  mulgnnp1  13103  mulgnegnn  13105  mulgaddcom  13119  mulginvcom  13120  mulgnndir  13124  mulgnn0ass  13131  mhmmulg  13136  mulgpropdg  13137  subginv  13153  subgsub  13158  subgmulg  13160  eqglact  13197  ghmsub  13223  ghmmulg  13228  resghm  13232  ghmeql  13239  conjghm  13248  ablsub4  13285  ablsub32  13294  imasabl  13308  mgpress  13320  rngsubdi  13340  rngsubdir  13341  imasrng  13345  dfur2g  13351  srgass  13360  srgmulgass  13378  srgpcomp  13379  srglmhm  13382  srgrmhm  13383  crngcom  13403  ringass  13405  ringcom  13420  ringsubdi  13443  ringsubdir  13444  mulgass2  13445  ringlghm  13448  ringrghm  13449  imasring  13451  opprrng  13464  opprring  13466  oppr0g  13468  oppr1g  13469  opprnegg  13470  mulgass3  13472  dvdsrvald  13480  unitlinv  13513  unitrinv  13514  dvrfvald  13520  dvrass  13526  dvrdir  13530  rdivmuldivd  13531  rngidpropdg  13533  dvdsrpropdg  13534  unitpropdg  13535  invrpropdg  13536  rhm1  13554  rhmopp  13563  subrguss  13620  subrginv  13621  subrgdv  13622  lmodcom  13692  lmodsubdir  13704  rmodislmod  13710  lsppropd  13791  srascag  13801  sravscag  13802  ixpsnbasval  13825  rsp0  13852  lidlrsppropdg  13854  rnglidlmsgrp  13856  mulgghm2  13952  mulgrhm  13953  zlmlemg  13972  zlmsca  13976  znle  13981  psrbasg  14012  psrplusgg  14015  tgdom  14093  txbasval  14288  cnmpt11  14304  cnmpt21  14312  setsmsbasg  14500  bdbl  14524  dvmulxxbr  14704  dvimulf  14708  dvcj  14711  dvfre  14712  dvrecap  14715  dvef  14726  sinperlem  14767  coshalfpip  14781  ptolemy  14783  tangtx  14797  relogef  14823  rpcxpadd  14864  rpmulcxp  14868  rpdivcxp  14870  cxpmul  14871  abscxp  14873  rpcxpsqrt  14880  rpabscxpbnd  14897  rplogbreexp  14909  rprelogbmul  14911  rprelogbdiv  14913  lgsneg  14964  lgsmod  14966  lgsdir2  14973  lgsdirprm  14974  lgsdir  14975  lgsdi  14977  lgssq  14980  lgssq2  14981  lgsdirnn0  14987  lgsdinn0  14988  lgseisenlem1  14989  2sqlem3  15003  bj-charfundcALT  15100  nninfsellemeqinf  15305  refeq  15317