Theorem 3eqtr4rd 2791

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd

Step	Hyp	Ref	Expression
1		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
2		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr4d 2783	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2783	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  csbun  4464  csbdif  4547  csbcnvgALT  5909  csbres  6012  fimacnvinrn2  7106  f1ossf1o  7162  suppvalbr  8205  odi  8635  phplem2  9271  phplem4OLD  9283  cantnfp1lem3  9749  cantnfp1  9750  cardidm  10028  ackbij2lem2  10308  ackbij2lem3  10309  divneg  11986  xadddilem  13356  xadddi2  13359  dfceil2  13890  modlt  13931  modmulnn  13940  seqcaopr3  14088  bcval5  14367  hashgadd  14426  hashun3  14433  hashmap  14484  seqcoll  14513  revccat  14814  cshwmodn  14843  2cshwcom  14864  cshimadifsn0  14879  revco  14883  cshco  14885  ofccat  15018  relexpsucl  15080  dfrtrclrec2  15107  cjreb  15172  recj  15173  imcj  15181  imval2  15200  sqrtmul  15308  absmax  15378  amgm2  15418  summolem2a  15763  fsumf1o  15771  sumsnf  15791  sumsplit  15816  fsummulc2  15832  binom  15878  bcxmas  15883  incexclem  15884  incexc  15885  expcnv  15912  pwdif  15916  cvgrat  15931  prodmolem3  15981  prodmolem2a  15982  fprodf1o  15994  prodsn  16010  prodsnf  16012  fprodabs  16022  binomfallfac  16089  fallfacval4  16091  bcfallfac  16092  ege2le3  16138  efaddlem  16141  eftlub  16157  tanval3  16182  tanneg  16196  cosmul  16221  cos01bnd  16234  demoivreALT  16249  flodddiv4  16461  absmulgcd  16596  nn0expgcd  16611  lcmfunsnlem2  16687  eulerthlem2  16829  phisum  16837  pythagtriplem14  16875  pythagtriplem19  16880  pcmul  16898  pcfac  16946  prmreclem6  16968  4sqlem12  17003  vdwlem6  17033  oppccatid  17779  curf2ndf  18317  oppcyon  18339  joincomALT  18471  meetcomALT  18473  pwsco1mhm  18867  sgrp2nmndlem4  18963  qusgrp2  19098  mulgnngsum  19119  mulgnn0p1  19125  mulgneg  19132  mulgnn0dir  19144  qusghm  19295  gaid  19339  symgval  19412  pmtrdifellem3  19520  psgnunilem2  19537  odmulg  19598  sylow1lem2  19641  sylow2a  19661  sylow3lem1  19669  efgredleme  19785  efgcpbllemb  19797  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  ablsimpgfindlem1  20151  srgpcomp  20245  srgbinom  20258  rdivmuldivd  20439  c0mgm  20485  c0mhm  20486  zrrnghm  20562  imadrhmcl  20820  lmodvsmmulgdi  20917  lmodsubdi  20939  rmodislmodlem  20949  0lmhm  21062  lspsneq  21147  qusrhm  21309  quscrng  21316  zringlpirlem3  21498  mulgrhm  21511  phssip  21699  frlmip  21821  frlmphl  21824  asclmulg  21945  resspsrmul  22019  evlsscasrng  22144  psdadd  22190  psdvsca  22191  psdmul  22193  psropprmul  22260  evls1scasrng  22364  mat1ghm  22510  mat1mhm  22511  1marepvmarrepid  22602  mdetrlin  22629  mdetrsca2  22631  mdetunilem7  22645  mdetunilem9  22647  mndifsplit  22663  maducoeval2  22667  smadiadetglem2  22699  decpmatmul  22799  pm2mpghm  22843  pm2mpmhmlem2  22846  cpmidgsum2  22906  ptbasfi  23610  ptuni  23623  alexsubALTlem3  24078  subgtgp  24134  tsmsxplem1  24182  xmsusp  24603  restmetu  24604  nminv  24655  nrginvrcnlem  24733  copco  25070  pcoass  25076  pi1bas  25090  pi1xfrf  25105  pi1xfr  25107  isclmp  25149  cph2subdi  25263  cphassr  25265  tcphcphlem1  25288  cphipval  25296  rrxip  25443  rrxnm  25444  pjthlem1  25490  ovolunlem1a  25550  ovolfs2  25625  uniiccdif  25632  ismbf  25682  itgaddlem2  25879  ditgswap  25914  ply1divex  26196  plyeq0lem  26269  plymullem1  26273  dgrcolem1  26333  dgrcolem2  26334  vieta1lem2  26371  elqaalem2  26380  elqaalem3  26381  aaliou3lem7  26409  ulmshft  26451  mulcxplem  26744  cxpmul2  26749  root1eq1  26816  cxpeq  26818  logbchbase  26832  cosangneg2d  26868  isosctrlem2  26880  angpieqvdlem  26889  chordthmlem3  26895  chordthmlem4  26896  chordthmlem5  26897  quad2  26900  dcubic2  26905  cubic2  26909  quart1  26917  scvxcvx  27047  igamlgam  27111  lgam1  27125  basellem9  27150  ppifl  27221  mumul  27242  sgmmul  27263  chtublem  27273  chpub  27282  logfacrlim  27286  dchrsum2  27330  sumdchr2  27332  bposlem9  27354  lgsdir2  27392  lgsdir  27394  lgsdi  27396  lgsdirnn0  27406  lgsdinn0  27407  lgsquad3  27449  2sqblem  27493  chpo1ub  27542  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2if  27559  dchrisum0fmul  27568  rpvmasum2  27574  mulog2sumlem1  27596  vmalogdivsum2  27600  log2sumbnd  27606  selberg3lem1  27619  selberg4lem1  27622  pntrsumo1  27627  selbergr  27630  pntpbnd1  27648  pntlemk  27668  mulsunif2lem  28213  divsasswd  28246  absmuls  28286  zscut  28411  expsp1  28430  tgbtwnconn1lem3  28600  mideulem2  28760  axlowdimlem16  28990  axcontlem8  29004  vtxval  29035  iedgval  29036  edgval  29084  vtxdgop  29506  finsumvtxdg2size  29586  lp1cycl  30184  ex-ind-dvds  30493  vsfval  30665  lnocoi  30789  nmblolbii  30831  ipasslem5  30867  hvsubid  31058  sshjval3  31386  pjhthlem1  31423  adjval  31922  unopf1o  31948  kbpj  31988  lnopmi  32032  nmcoplbi  32060  cnlnadjlem2  32100  adjadd  32125  branmfn  32137  pjtoi  32211  ofoprabco  32682  supppreima  32703  hashxpe  32814  ccatws1f1o  32918  splfv3  32925  xrsmulgzz  32992  mndractfo  33015  mndlactf1o  33016  mndractf1o  33017  psgnfzto1stlem  33093  cycpmco2lem5  33123  cycpmco2lem6  33124  cyc3co2  33133  tocyccntz  33137  cyc3genpmlem  33144  cyc3conja  33150  archiabllem1a  33171  gsumvsca1  33205  gsumvsca2  33206  rloccring  33242  imaslmod  33346  elrspunidl  33421  mxidlirredi  33464  opprabs  33475  qsdrngi  33488  1arithidomlem1  33528  1arithidomlem2  33529  zringfrac  33547  ply1degltdimlem  33635  fedgmullem1  33642  algextdeglem4  33711  constrconj  33735  submat1n  33751  submatres  33752  madjusmdetlem3  33775  xrge0iifhom  33883  qqhval2lem  33927  qqhrhm  33935  qqhucn  33938  esumsnf  34028  measvunilem0  34177  carsgclctunlem1  34282  ballotlemfp1  34456  ballotlemsf1o  34478  signstfveq0  34554  breprexplemc  34609  breprexp  34610  breprexpnat  34611  circlemeth  34617  logdivsqrle  34627  hgt750lema  34634  revwlk  35092  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3lem5  35291  cvmlift3lem6  35292  cvmlift3lem9  35295  elmrsubrn  35488  bccolsum  35701  bj-bary1lem  37276  finixpnum  37565  poimirlem4  37584  poimirlem16  37596  poimirlem19  37599  poimirlem25  37605  mblfinlem3  37619  dvtan  37630  itg2addnc  37634  itgaddnclem2  37639  ftc1anclem6  37658  areacirclem5  37672  areacirc  37673  upixp  37689  prdsbnd2  37755  ismrer1  37798  rngoneglmul  37903  rngoisocnv  37941  islshpsm  38936  lshpnel2N  38941  lfl0f  39025  ldualvsdi1  39099  ldualgrplem  39101  cmtcomlemN  39204  cvlsupr8  39305  pmodl42N  39808  pmapjat1  39810  llnmod2i2  39820  dalawlem2  39829  pmapj2N  39886  idltrn  40107  cdlemc6  40153  cdleme20d  40269  cdleme22e  40301  cdleme22eALTN  40302  cdleme35b  40407  cdleme48fvg  40457  cdlemg4d  40570  cdlemg8a  40584  cdlemg42  40686  cdlemg47a  40691  tendodi1  40741  tendodi2  40742  cdlemk4  40791  cdlemk21N  40830  cdlemk22  40850  cdlemky  40883  cdlemk53b  40913  cdlemk53  40914  cdlemkyyN  40919  erngdvlem3-rN  40955  tendocnv  40978  dia1dim2  41019  dicvaddcl  41147  dihglblem3N  41252  dihmeetlem4preN  41263  dihmeet2  41303  lcfl7lem  41456  baerlem3lem1  41664  baerlem5alem1  41665  mapdh6bN  41694  mapdh6cN  41695  mapdh6dN  41696  hdmap1l6b  41768  hdmap1l6c  41769  hdmap1l6d  41770  hdmap14lem13  41837  ofun  42231  grpcominv1  42463  evlselv  42542  flt4lem7  42614  3cubeslem2  42641  3cubeslem3r  42643  3cubeslem4  42645  pellexlem2  42786  rmxyneg  42877  oddcomabszz  42901  acongeq  42940  hausgraph  43166  onsupnmax  43189  tfsconcatrev  43310  naddass1  43355  fsovrfovd  43971  inductionexd  44117  expgrowth  44304  binomcxplemwb  44317  binomcxplemnn0  44318  binomcxplemnotnn0  44325  sumsnd  44926  restuni4  45023  fmuldfeqlem1  45503  cncfmptss  45508  climexp  45526  dvresntr  45839  stoweidlem17  45938  wallispi  45991  dirkertrigeq  46022  dirkercncflem2  46025  fourierdlem30  46058  fourierdlem41  46069  fourierdlem81  46108  fourierdlem103  46130  sge0xp  46350  sge0isummpt2  46353  isomennd  46452  vonioolem1  46601  sigarperm  46781  fcores  46982  imasetpreimafvbijlemfo  47279  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjimaid  47285  prprspr2  47392  opoeALTV  47557  uhgrimisgrgric  47783  cznrng  47984  rngchomrnghmresALTV  48002  fdmdifeqresdif  48066  lincsum  48158  lincscm  48159  lmod1lem4  48219  blennngt2o2  48326  blennn0e2  48328  topdlat  48676  reccot  48850  rectan  48851  cotsqcscsq  48854  amgmlemALT  48897