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  5692  fvco2  5702  resfunexg  5859  fcof1  5906  fliftfun  5919  caovdir2d  6181  caov32d  6185  caov31d  6187  caov4d  6189  caovlem2d  6197  caofcom  6247  caofdig  6250  cnvf1olem  6368  tfrlem1  6452  tfrlemisucaccv  6469  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  frecrdg  6552  oav2  6607  omv2  6609  omsuc  6616  nnmsucr  6632  ecovicom  6788  ecoviass  6790  ecovidi  6792  nnnninfeq  7291  nninfwlpoimlemg  7338  carden2bex  7358  addcompig  7512  addasspig  7513  mulcompig  7514  mulasspig  7515  distrpig  7516  addassnqg  7565  addnq0mo  7630  mulnq0mo  7631  nqnq0a  7637  nqnq0m  7638  distrnq0  7642  mulcomnq0  7643  addassnq0  7645  addcmpblnr  7922  mulcmpblnrlemg  7923  addsrmo  7926  mulsrmo  7927  ltsrprg  7930  recexgt0sr  7956  mulgt0sr  7961  mulextsr1lem  7963  addcnsrec  8025  mulcnsrec  8026  pitonnlem2  8030  recidpirqlemcalc  8040  axaddcom  8053  adddir  8133  mul32  8272  mul31  8273  add32  8301  add4  8303  sub32  8376  sub4  8387  subdir  8528  mulneg2  8538  mulreim  8747  apadd1  8751  apneg  8754  divassap  8833  divdirap  8840  divmul13ap  8858  divmul24ap  8859  divdiv32ap  8863  conjmulap  8872  zeo  9548  xaddcom  10053  xnegdi  10060  xaddass  10061  xaddass2  10062  xpncan  10063  xadd4d  10077  lincmb01cmp  10195  iccf1o  10196  flhalf  10517  modqvalp1  10560  modqdi  10609  modqsubdir  10610  frecuzrdgg  10633  seq3shft2  10698  seqshft2g  10699  seq3caopr3  10708  seqcaopr3g  10709  seq3caopr  10712  seqcaoprg  10713  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  seqf1oglem2a  10735  seqf1oglem2  10737  seqf1og  10738  seq3homo  10744  seqfeq3  10746  seqhomog  10747  seqfeq4g  10748  seq3distr  10749  expp1  10763  expnegap0  10764  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  sqneg  10815  sqdivap  10820  subsq2  10864  binom2  10868  modqexp  10883  facp1  10947  bcm1k  10977  bcp1n  10978  bcval5  10980  omgadd  11019  hashun  11022  hashxp  11043  csbwrdg  11096  ccatass  11138  lswccatn0lsw  11141  swrdlsw  11196  swrdswrd  11232  wrd2ind  11250  swrdccatin1  11252  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccatpfx1  11263  swrdccat3blem  11266  cats1catd  11295  shftfibg  11326  shftfib  11329  shftval  11331  2shfti  11337  seq3shft  11344  crre  11363  remim  11366  mulreap  11370  reneg  11374  readd  11375  remullem  11377  redivap  11380  imneg  11382  imadd  11383  imdivap  11387  cjcj  11389  cjadd  11390  cjmulrcl  11393  cjneg  11396  imval2  11400  resqrexlemcalc1  11520  absneg  11556  sqabsadd  11561  sqabssub  11562  absmul  11575  absresq  11584  absexp  11585  absexpzap  11586  bdtrilem  11745  xrmaxiflemcom  11755  xrmaxadd  11767  xrminrecl  11779  xrminadd  11781  serf0  11858  summodclem3  11886  fsum3  11893  isumss  11897  fisumss  11898  fsumadd  11912  isummulc1  11933  isumdivapc  11934  fsum2dlemstep  11940  fisumcom2  11944  fisum0diag2  11953  fsummulc2  11954  fsummulc1  11955  fsumdivapc  11956  fsumconst  11960  telfsumo  11972  fsumparts  11976  binomlem  11989  isumshft  11996  arisum2  12005  geolim  12017  geo2sum  12020  geo2lim  12022  cvgratnnlemseq  12032  cvgratz  12038  mertenslem2  12042  prodfrecap  12052  prodfdivap  12053  prodmodclem2a  12082  fprodntrivap  12090  fprodssdc  12096  fprodmul  12097  fprodabs  12122  fprod2dlemstep  12128  fprodcom2fi  12132  fprodrec  12135  efcllemp  12164  efcj  12179  efexp  12188  resinval  12221  recosval  12222  cosneg  12233  efival  12238  sinadd  12242  cosadd  12243  addcos  12252  sin2t  12255  cos2t  12256  dvdsmodexp  12301  odd2np1lem  12378  oexpneg  12383  neggcd  12499  gcdabs2  12506  mulgcd  12532  mulgcdr  12534  gcddiv  12535  rplpwr  12543  eucalgval  12571  eucalginv  12573  eucalg  12576  neglcm  12592  lcmgcd  12595  mulgcddvds  12611  qredeu  12614  nn0gcdsq  12717  phimullem  12742  prmdiv  12752  coprimeprodsq  12775  pythagtriplem1  12783  pythagtriplem3  12785  pythagtriplem4  12786  pythagtriplem12  12793  pceulem  12812  pceu  12813  pcqmul  12821  pcexp  12827  pcneg  12843  pcadd  12858  pcmpt  12861  pcmpt2  12862  pcbc  12869  4sqlem7  12902  4sqlem10  12905  mul4sqlem  12911  4sqlem11  12919  ennnfonelemp1  12972  setsabsd  13066  setscom  13067  ressbasd  13095  strressid  13099  ressinbasd  13102  ressressg  13103  ressplusgd  13157  prdsval  13301  pwsplusgval  13323  pwsmulrval  13324  imasival  13334  qusin  13354  fvprif  13371  xpsfeq  13373  grpidpropdg  13402  gsumpropd  13420  gsumpropd2  13421  gsumress  13423  prdssgrpd  13443  mnd32g  13455  mnd4g  13457  prdsidlem  13475  prdsmndd  13476  pws0g  13479  imasmnd2  13480  0mhm  13514  resmhm  13515  mhmco  13518  gsumwmhm  13526  grpinvcnv  13596  grpinvpropdg  13603  grpinvsub  13610  grpaddsubass  13618  grpsubpropdg  13632  grpsubpropd2  13633  prdsinvlem  13636  pwsinvg  13640  pwssub  13641  imasgrp2  13642  imasgrp  13643  qusgrp2  13645  mulgnnp1  13662  mulgnegnn  13664  mulgaddcom  13678  mulginvcom  13679  mulgnndir  13683  mulgnn0ass  13690  mhmmulg  13695  mulgpropdg  13696  submmulg  13698  subginv  13713  subgsub  13718  subgmulg  13720  eqglact  13757  ghmsub  13783  ghmmulg  13788  resghm  13792  ghmeql  13799  conjghm  13808  ablsub4  13845  ablsub32  13854  imasabl  13868  gsumfzreidx  13869  gsumfzmptfidmadd  13871  gsumfzconst  13873  mgpress  13889  rngsubdi  13909  rngsubdir  13910  imasrng  13914  dfur2g  13920  srgass  13929  srgmulgass  13947  srgpcomp  13948  srglmhm  13951  srgrmhm  13952  crngcom  13972  ringass  13974  ringcom  13989  ringsubdi  14014  ringsubdir  14015  mulgass2  14016  ringlghm  14019  ringrghm  14020  imasring  14022  opprrng  14035  opprring  14037  oppr0g  14039  oppr1g  14040  opprnegg  14041  mulgass3  14043  dvdsrvald  14051  unitlinv  14084  unitrinv  14085  dvrfvald  14091  dvrass  14097  dvrdir  14101  rdivmuldivd  14102  rngidpropdg  14104  dvdsrpropdg  14105  unitpropdg  14106  invrpropdg  14107  rhm1  14125  rhmopp  14134  subrguss  14194  subrginv  14195  subrgdv  14196  lmodcom  14291  lmodsubdir  14303  rmodislmod  14309  lsppropd  14390  srascag  14400  sravscag  14401  ixpsnbasval  14424  rsp0  14451  lidlrsppropdg  14453  rnglidlmsgrp  14455  gsumfzfsumlemm  14545  expghmap  14565  mulgghm2  14566  mulgrhm  14567  zlmlemg  14586  zlmsca  14590  znle  14595  psrbasg  14632  psrplusgg  14636  psrlinv  14642  tgdom  14740  txbasval  14935  cnmpt11  14951  cnmpt21  14959  setsmsbasg  15147  bdbl  15171  dvmulxxbr  15370  dvimulf  15374  dvcj  15377  dvfre  15378  dvrecap  15381  dvmptc  15385  dvmptfsum  15393  dvef  15395  plyaddlem1  15415  plyrecj  15431  dvply1  15433  sinperlem  15476  coshalfpip  15490  ptolemy  15492  tangtx  15506  relogef  15532  rpcxpadd  15573  rpmulcxp  15577  rpdivcxp  15579  cxpmul  15580  rpcxpmul2  15581  abscxp  15583  rpcxpsqrt  15590  rpabscxpbnd  15608  rplogbreexp  15621  rprelogbmul  15623  rprelogbdiv  15625  1sgmprm  15662  perfect1  15666  perfectlem2  15668  perfect  15669  lgsneg  15697  lgsmod  15699  lgsdir2  15706  lgsdirprm  15707  lgsdir  15708  lgsdi  15710  lgssq  15713  lgssq2  15714  lgsdirnn0  15720  lgsdinn0  15721  gausslemma2dlem6  15740  lgseisenlem1  15743  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlem1  15750  lgsquad2  15756  2sqlem3  15790  setsiedg  15847  bj-charfundcALT  16130  nninfsellemeqinf  16341  refeq  16355