Theorem 3eqtr4d 2249

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  fnsnfv  5651  fvco2  5661  resfunexg  5818  fcof1  5865  fliftfun  5878  caovdir2d  6136  caov32d  6140  caov31d  6142  caov4d  6144  caovlem2d  6152  caofcom  6202  caofdig  6205  cnvf1olem  6323  tfrlem1  6407  tfrlemisucaccv  6424  tfr1onlemsucaccv  6440  tfrcllemsucaccv  6453  frecrdg  6507  oav2  6562  omv2  6564  omsuc  6571  nnmsucr  6587  ecovicom  6743  ecoviass  6745  ecovidi  6747  nnnninfeq  7245  nninfwlpoimlemg  7292  carden2bex  7312  addcompig  7462  addasspig  7463  mulcompig  7464  mulasspig  7465  distrpig  7466  addassnqg  7515  addnq0mo  7580  mulnq0mo  7581  nqnq0a  7587  nqnq0m  7588  distrnq0  7592  mulcomnq0  7593  addassnq0  7595  addcmpblnr  7872  mulcmpblnrlemg  7873  addsrmo  7876  mulsrmo  7877  ltsrprg  7880  recexgt0sr  7906  mulgt0sr  7911  mulextsr1lem  7913  addcnsrec  7975  mulcnsrec  7976  pitonnlem2  7980  recidpirqlemcalc  7990  axaddcom  8003  adddir  8083  mul32  8222  mul31  8223  add32  8251  add4  8253  sub32  8326  sub4  8337  subdir  8478  mulneg2  8488  mulreim  8697  apadd1  8701  apneg  8704  divassap  8783  divdirap  8790  divmul13ap  8808  divmul24ap  8809  divdiv32ap  8813  conjmulap  8822  zeo  9498  xaddcom  10003  xnegdi  10010  xaddass  10011  xaddass2  10012  xpncan  10013  xadd4d  10027  lincmb01cmp  10145  iccf1o  10146  flhalf  10467  modqvalp1  10510  modqdi  10559  modqsubdir  10560  frecuzrdgg  10583  seq3shft2  10648  seqshft2g  10649  seq3caopr3  10658  seqcaopr3g  10659  seq3caopr  10662  seqcaoprg  10663  seq3f1olemqsumkj  10678  seq3f1olemqsumk  10679  seq3f1olemqsum  10680  seqf1oglem2a  10685  seqf1oglem2  10687  seqf1og  10688  seq3homo  10694  seqfeq3  10696  seqhomog  10697  seqfeq4g  10698  seq3distr  10699  expp1  10713  expnegap0  10714  expaddzaplem  10749  expaddzap  10750  expmulzap  10752  sqneg  10765  sqdivap  10770  subsq2  10814  binom2  10818  modqexp  10833  facp1  10897  bcm1k  10927  bcp1n  10928  bcval5  10930  omgadd  10969  hashun  10972  hashxp  10993  csbwrdg  11045  ccatass  11087  lswccatn0lsw  11090  swrdlsw  11145  swrdswrd  11181  wrd2ind  11199  shftfibg  11206  shftfib  11209  shftval  11211  2shfti  11217  seq3shft  11224  crre  11243  remim  11246  mulreap  11250  reneg  11254  readd  11255  remullem  11257  redivap  11260  imneg  11262  imadd  11263  imdivap  11267  cjcj  11269  cjadd  11270  cjmulrcl  11273  cjneg  11276  imval2  11280  resqrexlemcalc1  11400  absneg  11436  sqabsadd  11441  sqabssub  11442  absmul  11455  absresq  11464  absexp  11465  absexpzap  11466  bdtrilem  11625  xrmaxiflemcom  11635  xrmaxadd  11647  xrminrecl  11659  xrminadd  11661  serf0  11738  summodclem3  11766  fsum3  11773  isumss  11777  fisumss  11778  fsumadd  11792  isummulc1  11813  isumdivapc  11814  fsum2dlemstep  11820  fisumcom2  11824  fisum0diag2  11833  fsummulc2  11834  fsummulc1  11835  fsumdivapc  11836  fsumconst  11840  telfsumo  11852  fsumparts  11856  binomlem  11869  isumshft  11876  arisum2  11885  geolim  11897  geo2sum  11900  geo2lim  11902  cvgratnnlemseq  11912  cvgratz  11918  mertenslem2  11922  prodfrecap  11932  prodfdivap  11933  prodmodclem2a  11962  fprodntrivap  11970  fprodssdc  11976  fprodmul  11977  fprodabs  12002  fprod2dlemstep  12008  fprodcom2fi  12012  fprodrec  12015  efcllemp  12044  efcj  12059  efexp  12068  resinval  12101  recosval  12102  cosneg  12113  efival  12118  sinadd  12122  cosadd  12123  addcos  12132  sin2t  12135  cos2t  12136  dvdsmodexp  12181  odd2np1lem  12258  oexpneg  12263  neggcd  12379  gcdabs2  12386  mulgcd  12412  mulgcdr  12414  gcddiv  12415  rplpwr  12423  eucalgval  12451  eucalginv  12453  eucalg  12456  neglcm  12472  lcmgcd  12475  mulgcddvds  12491  qredeu  12494  nn0gcdsq  12597  phimullem  12622  prmdiv  12632  coprimeprodsq  12655  pythagtriplem1  12663  pythagtriplem3  12665  pythagtriplem4  12666  pythagtriplem12  12673  pceulem  12692  pceu  12693  pcqmul  12701  pcexp  12707  pcneg  12723  pcadd  12738  pcmpt  12741  pcmpt2  12742  pcbc  12749  4sqlem7  12782  4sqlem10  12785  mul4sqlem  12791  4sqlem11  12799  ennnfonelemp1  12852  setsabsd  12946  setscom  12947  ressbasd  12974  strressid  12978  ressinbasd  12981  ressressg  12982  ressplusgd  13036  prdsval  13180  pwsplusgval  13202  pwsmulrval  13203  imasival  13213  qusin  13233  fvprif  13250  xpsfeq  13252  grpidpropdg  13281  gsumpropd  13299  gsumpropd2  13300  gsumress  13302  prdssgrpd  13322  mnd32g  13334  mnd4g  13336  prdsidlem  13354  prdsmndd  13355  pws0g  13358  imasmnd2  13359  0mhm  13393  resmhm  13394  mhmco  13397  gsumwmhm  13405  grpinvcnv  13475  grpinvpropdg  13482  grpinvsub  13489  grpaddsubass  13497  grpsubpropdg  13511  grpsubpropd2  13512  prdsinvlem  13515  pwsinvg  13519  pwssub  13520  imasgrp2  13521  imasgrp  13522  qusgrp2  13524  mulgnnp1  13541  mulgnegnn  13543  mulgaddcom  13557  mulginvcom  13558  mulgnndir  13562  mulgnn0ass  13569  mhmmulg  13574  mulgpropdg  13575  submmulg  13577  subginv  13592  subgsub  13597  subgmulg  13599  eqglact  13636  ghmsub  13662  ghmmulg  13667  resghm  13671  ghmeql  13678  conjghm  13687  ablsub4  13724  ablsub32  13733  imasabl  13747  gsumfzreidx  13748  gsumfzmptfidmadd  13750  gsumfzconst  13752  mgpress  13768  rngsubdi  13788  rngsubdir  13789  imasrng  13793  dfur2g  13799  srgass  13808  srgmulgass  13826  srgpcomp  13827  srglmhm  13830  srgrmhm  13831  crngcom  13851  ringass  13853  ringcom  13868  ringsubdi  13893  ringsubdir  13894  mulgass2  13895  ringlghm  13898  ringrghm  13899  imasring  13901  opprrng  13914  opprring  13916  oppr0g  13918  oppr1g  13919  opprnegg  13920  mulgass3  13922  dvdsrvald  13930  unitlinv  13963  unitrinv  13964  dvrfvald  13970  dvrass  13976  dvrdir  13980  rdivmuldivd  13981  rngidpropdg  13983  dvdsrpropdg  13984  unitpropdg  13985  invrpropdg  13986  rhm1  14004  rhmopp  14013  subrguss  14073  subrginv  14074  subrgdv  14075  lmodcom  14170  lmodsubdir  14182  rmodislmod  14188  lsppropd  14269  srascag  14279  sravscag  14280  ixpsnbasval  14303  rsp0  14330  lidlrsppropdg  14332  rnglidlmsgrp  14334  gsumfzfsumlemm  14424  expghmap  14444  mulgghm2  14445  mulgrhm  14446  zlmlemg  14465  zlmsca  14469  znle  14474  psrbasg  14511  psrplusgg  14515  psrlinv  14521  tgdom  14619  txbasval  14814  cnmpt11  14830  cnmpt21  14838  setsmsbasg  15026  bdbl  15050  dvmulxxbr  15249  dvimulf  15253  dvcj  15256  dvfre  15257  dvrecap  15260  dvmptc  15264  dvmptfsum  15272  dvef  15274  plyaddlem1  15294  plyrecj  15310  dvply1  15312  sinperlem  15355  coshalfpip  15369  ptolemy  15371  tangtx  15385  relogef  15411  rpcxpadd  15452  rpmulcxp  15456  rpdivcxp  15458  cxpmul  15459  rpcxpmul2  15460  abscxp  15462  rpcxpsqrt  15469  rpabscxpbnd  15487  rplogbreexp  15500  rprelogbmul  15502  rprelogbdiv  15504  1sgmprm  15541  perfect1  15545  perfectlem2  15547  perfect  15548  lgsneg  15576  lgsmod  15578  lgsdir2  15585  lgsdirprm  15586  lgsdir  15587  lgsdi  15589  lgssq  15592  lgssq2  15593  lgsdirnn0  15599  lgsdinn0  15600  gausslemma2dlem6  15619  lgseisenlem1  15622  lgseisenlem3  15624  lgseisenlem4  15625  lgsquadlem1  15629  lgsquad2  15635  2sqlem3  15669  bj-charfundcALT  15883  nninfsellemeqinf  16094  refeq  16108