Theorem 3eqtr4d 2272

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  fnsnfv  5701  fvco2  5711  resfunexg  5870  fcof1  5919  fliftfun  5932  caovdir2d  6194  caov32d  6198  caov31d  6200  caov4d  6202  caovlem2d  6210  caofcom  6261  caofdig  6264  cnvf1olem  6384  tfrlem1  6469  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  frecrdg  6569  oav2  6626  omv2  6628  omsuc  6635  nnmsucr  6651  ecovicom  6807  ecoviass  6809  ecovidi  6811  nnnninfeq  7318  nninfwlpoimlemg  7365  carden2bex  7385  addcompig  7539  addasspig  7540  mulcompig  7541  mulasspig  7542  distrpig  7543  addassnqg  7592  addnq0mo  7657  mulnq0mo  7658  nqnq0a  7664  nqnq0m  7665  distrnq0  7669  mulcomnq0  7670  addassnq0  7672  addcmpblnr  7949  mulcmpblnrlemg  7950  addsrmo  7953  mulsrmo  7954  ltsrprg  7957  recexgt0sr  7983  mulgt0sr  7988  mulextsr1lem  7990  addcnsrec  8052  mulcnsrec  8053  pitonnlem2  8057  recidpirqlemcalc  8067  axaddcom  8080  adddir  8160  mul32  8299  mul31  8300  add32  8328  add4  8330  sub32  8403  sub4  8414  subdir  8555  mulneg2  8565  mulreim  8774  apadd1  8778  apneg  8781  divassap  8860  divdirap  8867  divmul13ap  8885  divmul24ap  8886  divdiv32ap  8890  conjmulap  8899  zeo  9575  xaddcom  10086  xnegdi  10093  xaddass  10094  xaddass2  10095  xpncan  10096  xadd4d  10110  lincmb01cmp  10228  iccf1o  10229  flhalf  10552  modqvalp1  10595  modqdi  10644  modqsubdir  10645  frecuzrdgg  10668  seq3shft2  10733  seqshft2g  10734  seq3caopr3  10743  seqcaopr3g  10744  seq3caopr  10747  seqcaoprg  10748  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seqf1oglem2a  10770  seqf1oglem2  10772  seqf1og  10773  seq3homo  10779  seqfeq3  10781  seqhomog  10782  seqfeq4g  10783  seq3distr  10784  expp1  10798  expnegap0  10799  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  sqneg  10850  sqdivap  10855  subsq2  10899  binom2  10903  modqexp  10918  facp1  10982  bcm1k  11012  bcp1n  11013  bcval5  11015  omgadd  11055  hashun  11058  hashxp  11080  csbwrdg  11133  ccatass  11175  lswccatn0lsw  11178  swrdlsw  11240  swrdswrd  11276  wrd2ind  11294  swrdccatin1  11296  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatpfx1  11307  swrdccat3blem  11310  cats1catd  11339  shftfibg  11371  shftfib  11374  shftval  11376  2shfti  11382  seq3shft  11389  crre  11408  remim  11411  mulreap  11415  reneg  11419  readd  11420  remullem  11422  redivap  11425  imneg  11427  imadd  11428  imdivap  11432  cjcj  11434  cjadd  11435  cjmulrcl  11438  cjneg  11441  imval2  11445  resqrexlemcalc1  11565  absneg  11601  sqabsadd  11606  sqabssub  11607  absmul  11620  absresq  11629  absexp  11630  absexpzap  11631  bdtrilem  11790  xrmaxiflemcom  11800  xrmaxadd  11812  xrminrecl  11824  xrminadd  11826  serf0  11903  summodclem3  11931  fsum3  11938  isumss  11942  fisumss  11943  fsumadd  11957  isummulc1  11978  isumdivapc  11979  fsum2dlemstep  11985  fisumcom2  11989  fisum0diag2  11998  fsummulc2  11999  fsummulc1  12000  fsumdivapc  12001  fsumconst  12005  telfsumo  12017  fsumparts  12021  binomlem  12034  isumshft  12041  arisum2  12050  geolim  12062  geo2sum  12065  geo2lim  12067  cvgratnnlemseq  12077  cvgratz  12083  mertenslem2  12087  prodfrecap  12097  prodfdivap  12098  prodmodclem2a  12127  fprodntrivap  12135  fprodssdc  12141  fprodmul  12142  fprodabs  12167  fprod2dlemstep  12173  fprodcom2fi  12177  fprodrec  12180  efcllemp  12209  efcj  12224  efexp  12233  resinval  12266  recosval  12267  cosneg  12278  efival  12283  sinadd  12287  cosadd  12288  addcos  12297  sin2t  12300  cos2t  12301  dvdsmodexp  12346  odd2np1lem  12423  oexpneg  12428  neggcd  12544  gcdabs2  12551  mulgcd  12577  mulgcdr  12579  gcddiv  12580  rplpwr  12588  eucalgval  12616  eucalginv  12618  eucalg  12621  neglcm  12637  lcmgcd  12640  mulgcddvds  12656  qredeu  12659  nn0gcdsq  12762  phimullem  12787  prmdiv  12797  coprimeprodsq  12820  pythagtriplem1  12828  pythagtriplem3  12830  pythagtriplem4  12831  pythagtriplem12  12838  pceulem  12857  pceu  12858  pcqmul  12866  pcexp  12872  pcneg  12888  pcadd  12903  pcmpt  12906  pcmpt2  12907  pcbc  12914  4sqlem7  12947  4sqlem10  12950  mul4sqlem  12956  4sqlem11  12964  ennnfonelemp1  13017  setsabsd  13111  setscom  13112  ressbasd  13140  strressid  13144  ressinbasd  13147  ressressg  13148  ressplusgd  13202  prdsval  13346  pwsplusgval  13368  pwsmulrval  13369  imasival  13379  qusin  13399  fvprif  13416  xpsfeq  13418  grpidpropdg  13447  gsumpropd  13465  gsumpropd2  13466  gsumress  13468  prdssgrpd  13488  mnd32g  13500  mnd4g  13502  prdsidlem  13520  prdsmndd  13521  pws0g  13524  imasmnd2  13525  0mhm  13559  resmhm  13560  mhmco  13563  gsumwmhm  13571  grpinvcnv  13641  grpinvpropdg  13648  grpinvsub  13655  grpaddsubass  13663  grpsubpropdg  13677  grpsubpropd2  13678  prdsinvlem  13681  pwsinvg  13685  pwssub  13686  imasgrp2  13687  imasgrp  13688  qusgrp2  13690  mulgnnp1  13707  mulgnegnn  13709  mulgaddcom  13723  mulginvcom  13724  mulgnndir  13728  mulgnn0ass  13735  mhmmulg  13740  mulgpropdg  13741  submmulg  13743  subginv  13758  subgsub  13763  subgmulg  13765  eqglact  13802  ghmsub  13828  ghmmulg  13833  resghm  13837  ghmeql  13844  conjghm  13853  ablsub4  13890  ablsub32  13899  imasabl  13913  gsumfzreidx  13914  gsumfzmptfidmadd  13916  gsumfzconst  13918  mgpress  13934  rngsubdi  13954  rngsubdir  13955  imasrng  13959  dfur2g  13965  srgass  13974  srgmulgass  13992  srgpcomp  13993  srglmhm  13996  srgrmhm  13997  crngcom  14017  ringass  14019  ringcom  14034  ringsubdi  14059  ringsubdir  14060  mulgass2  14061  ringlghm  14064  ringrghm  14065  imasring  14067  opprrng  14080  opprring  14082  oppr0g  14084  oppr1g  14085  opprnegg  14086  mulgass3  14088  dvdsrvald  14097  unitlinv  14130  unitrinv  14131  dvrfvald  14137  dvrass  14143  dvrdir  14147  rdivmuldivd  14148  rngidpropdg  14150  dvdsrpropdg  14151  unitpropdg  14152  invrpropdg  14153  rhm1  14171  rhmopp  14180  subrguss  14240  subrginv  14241  subrgdv  14242  lmodcom  14337  lmodsubdir  14349  rmodislmod  14355  lsppropd  14436  srascag  14446  sravscag  14447  ixpsnbasval  14470  rsp0  14497  lidlrsppropdg  14499  rnglidlmsgrp  14501  gsumfzfsumlemm  14591  expghmap  14611  mulgghm2  14612  mulgrhm  14613  zlmlemg  14632  zlmsca  14636  znle  14641  psrbasg  14678  psrplusgg  14682  psrlinv  14688  tgdom  14786  txbasval  14981  cnmpt11  14997  cnmpt21  15005  setsmsbasg  15193  bdbl  15217  dvmulxxbr  15416  dvimulf  15420  dvcj  15423  dvfre  15424  dvrecap  15427  dvmptc  15431  dvmptfsum  15439  dvef  15441  plyaddlem1  15461  plyrecj  15477  dvply1  15479  sinperlem  15522  coshalfpip  15536  ptolemy  15538  tangtx  15552  relogef  15578  rpcxpadd  15619  rpmulcxp  15623  rpdivcxp  15625  cxpmul  15626  rpcxpmul2  15627  abscxp  15629  rpcxpsqrt  15636  rpabscxpbnd  15654  rplogbreexp  15667  rprelogbmul  15669  rprelogbdiv  15671  1sgmprm  15708  perfect1  15712  perfectlem2  15714  perfect  15715  lgsneg  15743  lgsmod  15745  lgsdir2  15752  lgsdirprm  15753  lgsdir  15754  lgsdi  15756  lgssq  15759  lgssq2  15760  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem6  15786  lgseisenlem1  15789  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlem1  15796  lgsquad2  15802  2sqlem3  15836  setsiedg  15893  vtxdeqd  16102  vtxdfifiun  16103  bj-charfundcALT  16340  nninfsellemeqinf  16554  refeq  16568