Theorem 3eqtr4rd 2840

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

Syntax hints:   → wi 4   = wceq 1520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786

This theorem is referenced by:  csbun  4299  csbcnvgALT  5633  csbres  5729  fimacnvinrn2  6697  f1ossf1o  6744  odi  8046  phplem4  8536  cantnfp1lem3  8978  cantnfp1  8979  cardidm  9223  ackbij2lem2  9497  ackbij2lem3  9498  divneg  11169  xadddilem  12526  xadddi2  12529  dfceil2  13047  modlt  13086  modmulnn  13095  seqcaopr3  13243  bcval5  13516  hashgadd  13574  hashun3  13581  hashmap  13632  seqcoll  13658  cshwmodn  13981  2cshwcom  14002  cshimadifsn0  14016  revco  14020  cshco  14022  ofccat  14151  relexpsucl  14214  cjreb  14304  recj  14305  imcj  14313  imval2  14332  sqrtmul  14441  absmax  14511  amgm2  14551  summolem2a  14893  fsumf1o  14901  sumsnf  14920  sumsplit  14944  fsummulc2  14960  binom  15006  bcxmas  15011  incexclem  15012  incexc  15013  expcnv  15040  pwdif  15044  cvgrat  15060  prodmolem3  15108  prodmolem2a  15109  fprodf1o  15121  prodsn  15137  prodsnf  15139  fprodabs  15149  binomfallfac  15216  fallfacval4  15218  bcfallfac  15219  ege2le3  15264  efaddlem  15267  eftlub  15283  tanval3  15308  tanneg  15322  cosmul  15347  cos01bnd  15360  demoivreALT  15375  flodddiv4  15585  absmulgcd  15714  lcmfunsnlem2  15801  eulerthlem2  15936  phisum  15944  pythagtriplem14  15982  pythagtriplem19  15987  pcmul  16005  pcfac  16052  prmreclem6  16074  4sqlem12  16109  vdwlem6  16139  oppccatid  16806  curf2ndf  17314  oppcyon  17336  joincomALT  17456  meetcomALT  17458  pwsco1mhm  17797  sgrp2nmndlem4  17842  qusgrp2  17962  mulgnn0p1  17982  mulgneg  17989  mulgnn0dir  17999  qusghm  18124  gaid  18158  pmtrdifellem3  18325  psgnunilem2  18342  odmulg  18401  sylow1lem2  18442  sylow2a  18462  sylow3lem1  18470  efgredleme  18584  efgcpbllemb  18596  gsumzaddlem  18749  gsumconst  18762  gsumzmhm  18765  srgpcomp  18960  srgbinom  18973  lmodvsmmulgdi  19347  lmodsubdi  19369  rmodislmodlem  19379  0lmhm  19490  lspsneq  19572  qusrhm  19687  quscrng  19690  ascldimulOLD  19793  resspsrmul  19873  evlsscasrng  19981  psropprmul  20077  evls1scasrng  20172  zringlpirlem3  20303  mulgrhm  20315  phssip  20472  frlmip  20592  frlmphl  20595  mat1ghm  20764  mat1mhm  20765  1marepvmarrepid  20856  mdetrlin  20883  mdetrsca2  20885  mdetunilem7  20899  mdetunilem9  20901  mndifsplit  20917  maducoeval2  20921  smadiadetglem2  20953  decpmatmul  21052  pm2mpghm  21096  pm2mpmhmlem2  21099  cpmidgsum2  21159  ptbasfi  21861  ptuni  21874  alexsubALTlem3  22329  subgtgp  22385  tsmsxplem1  22432  xmsusp  22850  restmetu  22851  nminv  22901  nrginvrcnlem  22971  copco  23293  pcoass  23299  pi1bas  23313  pi1xfrf  23328  pi1xfr  23330  isclmp  23372  cph2subdi  23485  cphassr  23487  tcphcphlem1  23509  cphipval  23517  rrxip  23664  rrxnm  23665  pjthlem1  23711  ovolunlem1a  23768  ovolfs2  23843  uniiccdif  23850  ismbf  23900  itgaddlem2  24095  ditgswap  24128  ply1divex  24401  plyeq0lem  24471  plymullem1  24475  dgrcolem1  24534  dgrcolem2  24535  vieta1lem2  24571  elqaalem2  24580  elqaalem3  24581  aaliou3lem7  24609  ulmshft  24649  mulcxplem  24936  cxpmul2  24941  root1eq1  25005  cxpeq  25007  logbchbase  25018  cosangneg2d  25054  isosctrlem2  25066  angpieqvdlem  25075  chordthmlem3  25081  chordthmlem4  25082  chordthmlem5  25083  quad2  25086  dcubic2  25091  cubic2  25095  quart1  25103  scvxcvx  25233  igamlgam  25297  lgam1  25311  basellem9  25336  ppifl  25407  mumul  25428  sgmmul  25447  chtublem  25457  chpub  25466  logfacrlim  25470  dchrsum2  25514  sumdchr2  25516  bposlem9  25538  lgsdir2  25576  lgsdir  25578  lgsdi  25580  lgsdirnn0  25590  lgsdinn0  25591  lgsquad3  25633  2sqblem  25677  chpo1ub  25726  dchrmusum2  25740  dchrvmasumlem1  25741  dchrvmasum2if  25743  dchrisum0fmul  25752  rpvmasum2  25758  mulog2sumlem1  25780  vmalogdivsum2  25784  log2sumbnd  25790  selberg3lem1  25803  selberg4lem1  25806  pntrsumo1  25811  selbergr  25814  pntpbnd1  25832  pntlemk  25852  tgbtwnconn1lem3  26030  mideulem2  26190  axlowdimlem16  26414  axcontlem8  26428  vtxval  26456  iedgval  26457  edgval  26505  vtxdgop  26923  finsumvtxdg2size  27003  lp1cycl  27606  ex-ind-dvds  27920  vsfval  28089  lnocoi  28213  nmblolbii  28255  ipasslem5  28291  hvsubid  28482  sshjval3  28810  pjhthlem1  28847  adjval  29346  unopf1o  29372  kbpj  29412  lnopmi  29456  nmcoplbi  29484  cnlnadjlem2  29524  adjadd  29549  branmfn  29561  pjtoi  29635  ofoprabco  30072  hashxpe  30185  xrsmulgzz  30309  cyc3co2  30382  cyc3genpmlem  30389  cyc3conja  30395  archiabllem1a  30416  gsumvsca1  30455  gsumvsca2  30456  rdivmuldivd  30471  imaslmod  30531  fedgmullem1  30584  psgnfzto1stlem  30620  submat1n  30641  submatres  30642  madjusmdetlem3  30665  xrge0iifhom  30753  qqhval2lem  30795  qqhrhm  30803  qqhucn  30806  esumsnf  30896  measvunilem0  31045  carsgclctunlem1  31148  ballotlemfp1  31322  ballotlemsf1o  31344  signstfveq0  31420  breprexplemc  31476  breprexp  31477  breprexpnat  31478  circlemeth  31484  logdivsqrle  31494  hgt750lema  31501  cvmlift3lem2  32131  cvmlift3lem4  32133  cvmlift3lem5  32134  cvmlift3lem6  32135  cvmlift3lem9  32138  elmrsubrn  32320  bccolsum  32524  bj-bary1lem  34074  csbdif  34083  finixpnum  34354  poimirlem4  34373  poimirlem16  34385  poimirlem19  34388  poimirlem25  34394  mblfinlem3  34408  dvtan  34419  itg2addnc  34423  itgaddnclem2  34428  ftc1anclem6  34449  areacirclem5  34463  areacirc  34464  upixp  34482  prdsbnd2  34551  ismrer1  34594  rngoneglmul  34699  rngoisocnv  34737  islshpsm  35597  lshpnel2N  35602  lfl0f  35686  ldualvsdi1  35760  ldualgrplem  35762  cmtcomlemN  35865  cvlsupr8  35966  pmodl42N  36468  pmapjat1  36470  llnmod2i2  36480  dalawlem2  36489  pmapj2N  36546  idltrn  36767  cdlemc6  36813  cdleme20d  36929  cdleme22e  36961  cdleme22eALTN  36962  cdleme35b  37067  cdleme48fvg  37117  cdlemg4d  37230  cdlemg8a  37244  cdlemg42  37346  cdlemg47a  37351  tendodi1  37401  tendodi2  37402  cdlemk4  37451  cdlemk21N  37490  cdlemk22  37510  cdlemky  37543  cdlemk53b  37573  cdlemk53  37574  cdlemkyyN  37579  erngdvlem3-rN  37615  tendocnv  37638  dia1dim2  37679  dicvaddcl  37807  dihglblem3N  37912  dihmeetlem4preN  37923  dihmeet2  37963  lcfl7lem  38116  baerlem3lem1  38324  baerlem5alem1  38325  mapdh6bN  38354  mapdh6cN  38355  mapdh6dN  38356  hdmap1l6b  38428  hdmap1l6c  38429  hdmap1l6d  38430  hdmap14lem13  38497  nn0expgcd  38656  pellexlem2  38863  rmxyneg  38953  oddcomabszz  38977  acongeq  39016  hausgraph  39248  fsovrfovd  39791  inductionexd  39941  ablsimpgfindlem1  40117  expgrowth  40157  binomcxplemwb  40170  binomcxplemnn0  40171  binomcxplemnotnn0  40178  sumsnd  40774  restuni4  40880  fmuldfeqlem1  41359  cncfmptss  41364  climexp  41382  dvresntr  41697  stoweidlem17  41798  wallispi  41851  dirkertrigeq  41882  dirkercncflem2  41885  fourierdlem30  41918  fourierdlem41  41929  fourierdlem81  41968  fourierdlem103  41990  sge0xp  42207  sge0isummpt2  42210  isomennd  42309  vonioolem1  42458  sigarperm  42613  prprspr2  43116  opoeALTV  43284  c0mgm  43612  c0mhm  43613  zrrnghm  43620  cznrng  43658  rngchomrnghmresALTV  43699  fdmdifeqresdif  43822  lincsum  43918  lincscm  43919  lmod1lem4  43979  blennngt2o2  44087  blennn0e2  44089  reccot  44291  rectan  44292  cotsqcscsq  44295  amgmlemALT  44338