Theorem 3eqtr4d 2236

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

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

This theorem is referenced by:  fnsnfv  5616  fvco2  5626  resfunexg  5779  fcof1  5826  fliftfun  5839  caovdir2d  6095  caov32d  6099  caov31d  6101  caov4d  6103  caovlem2d  6111  caofcom  6156  caofdig  6159  cnvf1olem  6277  tfrlem1  6361  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  frecrdg  6461  oav2  6516  omv2  6518  omsuc  6525  nnmsucr  6541  ecovicom  6697  ecoviass  6699  ecovidi  6701  nnnninfeq  7187  nninfwlpoimlemg  7234  carden2bex  7249  addcompig  7389  addasspig  7390  mulcompig  7391  mulasspig  7392  distrpig  7393  addassnqg  7442  addnq0mo  7507  mulnq0mo  7508  nqnq0a  7514  nqnq0m  7515  distrnq0  7519  mulcomnq0  7520  addassnq0  7522  addcmpblnr  7799  mulcmpblnrlemg  7800  addsrmo  7803  mulsrmo  7804  ltsrprg  7807  recexgt0sr  7833  mulgt0sr  7838  mulextsr1lem  7840  addcnsrec  7902  mulcnsrec  7903  pitonnlem2  7907  recidpirqlemcalc  7917  axaddcom  7930  adddir  8010  mul32  8149  mul31  8150  add32  8178  add4  8180  sub32  8253  sub4  8264  subdir  8405  mulneg2  8415  mulreim  8623  apadd1  8627  apneg  8630  divassap  8709  divdirap  8716  divmul13ap  8734  divmul24ap  8735  divdiv32ap  8739  conjmulap  8748  zeo  9422  xaddcom  9927  xnegdi  9934  xaddass  9935  xaddass2  9936  xpncan  9937  xadd4d  9951  lincmb01cmp  10069  iccf1o  10070  flhalf  10371  modqvalp1  10414  modqdi  10463  modqsubdir  10464  frecuzrdgg  10487  seq3shft2  10552  seqshft2g  10553  seq3caopr3  10562  seqcaopr3g  10563  seq3caopr  10566  seqcaoprg  10567  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seqf1oglem2a  10589  seqf1oglem2  10591  seqf1og  10592  seq3homo  10598  seqfeq3  10600  seqhomog  10601  seqfeq4g  10602  seq3distr  10603  expp1  10617  expnegap0  10618  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  sqneg  10669  sqdivap  10674  subsq2  10718  binom2  10722  modqexp  10737  facp1  10801  bcm1k  10831  bcp1n  10832  bcval5  10834  omgadd  10873  hashun  10876  hashxp  10897  csbwrdg  10943  shftfibg  10964  shftfib  10967  shftval  10969  2shfti  10975  seq3shft  10982  crre  11001  remim  11004  mulreap  11008  reneg  11012  readd  11013  remullem  11015  redivap  11018  imneg  11020  imadd  11021  imdivap  11025  cjcj  11027  cjadd  11028  cjmulrcl  11031  cjneg  11034  imval2  11038  resqrexlemcalc1  11158  absneg  11194  sqabsadd  11199  sqabssub  11200  absmul  11213  absresq  11222  absexp  11223  absexpzap  11224  bdtrilem  11382  xrmaxiflemcom  11392  xrmaxadd  11404  xrminrecl  11416  xrminadd  11418  serf0  11495  summodclem3  11523  fsum3  11530  isumss  11534  fisumss  11535  fsumadd  11549  isummulc1  11570  isumdivapc  11571  fsum2dlemstep  11577  fisumcom2  11581  fisum0diag2  11590  fsummulc2  11591  fsummulc1  11592  fsumdivapc  11593  fsumconst  11597  telfsumo  11609  fsumparts  11613  binomlem  11626  isumshft  11633  arisum2  11642  geolim  11654  geo2sum  11657  geo2lim  11659  cvgratnnlemseq  11669  cvgratz  11675  mertenslem2  11679  prodfrecap  11689  prodfdivap  11690  prodmodclem2a  11719  fprodntrivap  11727  fprodssdc  11733  fprodmul  11734  fprodabs  11759  fprod2dlemstep  11765  fprodcom2fi  11769  fprodrec  11772  efcllemp  11801  efcj  11816  efexp  11825  resinval  11858  recosval  11859  cosneg  11870  efival  11875  sinadd  11879  cosadd  11880  addcos  11889  sin2t  11892  cos2t  11893  dvdsmodexp  11938  odd2np1lem  12013  oexpneg  12018  neggcd  12120  gcdabs2  12127  mulgcd  12153  mulgcdr  12155  gcddiv  12156  rplpwr  12164  eucalgval  12192  eucalginv  12194  eucalg  12197  neglcm  12213  lcmgcd  12216  mulgcddvds  12232  qredeu  12235  nn0gcdsq  12338  phimullem  12363  prmdiv  12373  coprimeprodsq  12395  pythagtriplem1  12403  pythagtriplem3  12405  pythagtriplem4  12406  pythagtriplem12  12413  pceulem  12432  pceu  12433  pcqmul  12441  pcexp  12447  pcneg  12463  pcadd  12478  pcmpt  12481  pcmpt2  12482  pcbc  12489  4sqlem7  12522  4sqlem10  12525  mul4sqlem  12531  4sqlem11  12539  ennnfonelemp1  12563  setsabsd  12657  setscom  12658  ressbasd  12685  strressid  12689  ressinbasd  12692  ressressg  12693  ressplusgd  12746  imasival  12889  qusin  12909  fvprif  12926  xpsfeq  12928  grpidpropdg  12957  gsumpropd  12975  gsumpropd2  12976  gsumress  12978  mnd32g  13008  mnd4g  13010  0mhm  13058  resmhm  13059  mhmco  13062  gsumwmhm  13070  grpinvcnv  13140  grpinvpropdg  13147  grpinvsub  13154  grpaddsubass  13162  grpsubpropdg  13176  grpsubpropd2  13177  imasgrp2  13180  imasgrp  13181  qusgrp2  13183  mulgnnp1  13200  mulgnegnn  13202  mulgaddcom  13216  mulginvcom  13217  mulgnndir  13221  mulgnn0ass  13228  mhmmulg  13233  mulgpropdg  13234  submmulg  13236  subginv  13251  subgsub  13256  subgmulg  13258  eqglact  13295  ghmsub  13321  ghmmulg  13326  resghm  13330  ghmeql  13337  conjghm  13346  ablsub4  13383  ablsub32  13392  imasabl  13406  gsumfzreidx  13407  gsumfzmptfidmadd  13409  gsumfzconst  13411  mgpress  13427  rngsubdi  13447  rngsubdir  13448  imasrng  13452  dfur2g  13458  srgass  13467  srgmulgass  13485  srgpcomp  13486  srglmhm  13489  srgrmhm  13490  crngcom  13510  ringass  13512  ringcom  13527  ringsubdi  13552  ringsubdir  13553  mulgass2  13554  ringlghm  13557  ringrghm  13558  imasring  13560  opprrng  13573  opprring  13575  oppr0g  13577  oppr1g  13578  opprnegg  13579  mulgass3  13581  dvdsrvald  13589  unitlinv  13622  unitrinv  13623  dvrfvald  13629  dvrass  13635  dvrdir  13639  rdivmuldivd  13640  rngidpropdg  13642  dvdsrpropdg  13643  unitpropdg  13644  invrpropdg  13645  rhm1  13663  rhmopp  13672  subrguss  13732  subrginv  13733  subrgdv  13734  lmodcom  13829  lmodsubdir  13841  rmodislmod  13847  lsppropd  13928  srascag  13938  sravscag  13939  ixpsnbasval  13962  rsp0  13989  lidlrsppropdg  13991  rnglidlmsgrp  13993  gsumfzfsumlemm  14075  expghmap  14095  mulgghm2  14096  mulgrhm  14097  zlmlemg  14116  zlmsca  14120  znle  14125  psrbasg  14159  psrplusgg  14162  tgdom  14240  txbasval  14435  cnmpt11  14451  cnmpt21  14459  setsmsbasg  14647  bdbl  14671  dvmulxxbr  14851  dvimulf  14855  dvcj  14858  dvfre  14859  dvrecap  14862  dvef  14873  plyaddlem1  14893  sinperlem  14943  coshalfpip  14957  ptolemy  14959  tangtx  14973  relogef  14999  rpcxpadd  15040  rpmulcxp  15044  rpdivcxp  15046  cxpmul  15047  abscxp  15049  rpcxpsqrt  15056  rpabscxpbnd  15073  rplogbreexp  15085  rprelogbmul  15087  rprelogbdiv  15089  lgsneg  15140  lgsmod  15142  lgsdir2  15149  lgsdirprm  15150  lgsdir  15151  lgsdi  15153  lgssq  15156  lgssq2  15157  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem6  15183  lgseisenlem1  15186  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  2sqlem3  15204  bj-charfundcALT  15301  nninfsellemeqinf  15506  refeq  15518