Theorem 3eqtr4rd 2785

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  csbun  4446  csbdif  4529  csbcnvgALT  5897  csbres  6002  fimacnvinrn2  7091  f1ossf1o  7147  suppvalbr  8187  odi  8615  phplem2  9242  phplem4OLD  9254  cantnfp1lem3  9717  cantnfp1  9718  cardidm  9996  ackbij2lem2  10276  ackbij2lem3  10277  divneg  11956  xadddilem  13332  xadddi2  13335  dfceil2  13875  modlt  13916  modmulnn  13925  seqcaopr3  14074  bcval5  14353  hashgadd  14412  hashun3  14419  hashmap  14470  seqcoll  14499  revccat  14800  cshwmodn  14829  2cshwcom  14850  cshimadifsn0  14865  revco  14869  cshco  14871  ofccat  15004  relexpsucl  15066  dfrtrclrec2  15093  cjreb  15158  recj  15159  imcj  15167  imval2  15186  sqrtmul  15294  absmax  15364  amgm2  15404  summolem2a  15747  fsumf1o  15755  sumsnf  15775  sumsplit  15800  fsummulc2  15816  binom  15862  bcxmas  15867  incexclem  15868  incexc  15869  expcnv  15896  pwdif  15900  cvgrat  15915  prodmolem3  15965  prodmolem2a  15966  fprodf1o  15978  prodsn  15994  prodsnf  15996  fprodabs  16006  binomfallfac  16073  fallfacval4  16075  bcfallfac  16076  ege2le3  16122  efaddlem  16125  eftlub  16141  tanval3  16166  tanneg  16180  cosmul  16205  cos01bnd  16218  demoivreALT  16233  flodddiv4  16448  absmulgcd  16582  nn0expgcd  16597  lcmfunsnlem2  16673  eulerthlem2  16815  phisum  16823  pythagtriplem14  16861  pythagtriplem19  16866  pcmul  16884  pcfac  16932  prmreclem6  16954  4sqlem12  16989  vdwlem6  17019  oppccatid  17765  curf2ndf  18303  oppcyon  18325  joincomALT  18458  meetcomALT  18460  pwsco1mhm  18857  sgrp2nmndlem4  18953  qusgrp2  19088  mulgnngsum  19109  mulgnn0p1  19115  mulgneg  19122  mulgnn0dir  19134  qusghm  19285  gaid  19329  symgval  19402  pmtrdifellem3  19510  psgnunilem2  19527  odmulg  19588  sylow1lem2  19631  sylow2a  19651  sylow3lem1  19659  efgredleme  19775  efgcpbllemb  19787  gsumzaddlem  19953  gsumconst  19966  gsumzmhm  19969  ablsimpgfindlem1  20141  srgpcomp  20235  srgbinom  20248  rdivmuldivd  20429  c0mgm  20475  c0mhm  20476  zrrnghm  20552  imadrhmcl  20814  lmodvsmmulgdi  20911  lmodsubdi  20933  rmodislmodlem  20943  0lmhm  21056  lspsneq  21141  qusrhm  21303  quscrng  21310  zringlpirlem3  21492  mulgrhm  21505  phssip  21693  frlmip  21815  frlmphl  21818  asclmulg  21939  resspsrmul  22013  evlsscasrng  22138  psdadd  22184  psdvsca  22185  psdmul  22187  psropprmul  22254  evls1scasrng  22358  mat1ghm  22504  mat1mhm  22505  1marepvmarrepid  22596  mdetrlin  22623  mdetrsca2  22625  mdetunilem7  22639  mdetunilem9  22641  mndifsplit  22657  maducoeval2  22661  smadiadetglem2  22693  decpmatmul  22793  pm2mpghm  22837  pm2mpmhmlem2  22840  cpmidgsum2  22900  ptbasfi  23604  ptuni  23617  alexsubALTlem3  24072  subgtgp  24128  tsmsxplem1  24176  xmsusp  24597  restmetu  24598  nminv  24649  nrginvrcnlem  24727  copco  25064  pcoass  25070  pi1bas  25084  pi1xfrf  25099  pi1xfr  25101  isclmp  25143  cph2subdi  25257  cphassr  25259  tcphcphlem1  25282  cphipval  25290  rrxip  25437  rrxnm  25438  pjthlem1  25484  ovolunlem1a  25544  ovolfs2  25619  uniiccdif  25626  ismbf  25676  itgaddlem2  25873  ditgswap  25908  ply1divex  26190  plyeq0lem  26263  plymullem1  26267  dgrcolem1  26327  dgrcolem2  26328  vieta1lem2  26367  elqaalem2  26376  elqaalem3  26377  aaliou3lem7  26405  ulmshft  26447  mulcxplem  26740  cxpmul2  26745  root1eq1  26812  cxpeq  26814  logbchbase  26828  cosangneg2d  26864  isosctrlem2  26876  angpieqvdlem  26885  chordthmlem3  26891  chordthmlem4  26892  chordthmlem5  26893  quad2  26896  dcubic2  26901  cubic2  26905  quart1  26913  scvxcvx  27043  igamlgam  27107  lgam1  27121  basellem9  27146  ppifl  27217  mumul  27238  sgmmul  27259  chtublem  27269  chpub  27278  logfacrlim  27282  dchrsum2  27326  sumdchr2  27328  bposlem9  27350  lgsdir2  27388  lgsdir  27390  lgsdi  27392  lgsdirnn0  27402  lgsdinn0  27403  lgsquad3  27445  2sqblem  27489  chpo1ub  27538  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasum2if  27555  dchrisum0fmul  27564  rpvmasum2  27570  mulog2sumlem1  27592  vmalogdivsum2  27596  log2sumbnd  27602  selberg3lem1  27615  selberg4lem1  27618  pntrsumo1  27623  selbergr  27626  pntpbnd1  27644  pntlemk  27664  mulsunif2lem  28209  divsasswd  28242  absmuls  28282  zscut  28407  expsp1  28426  tgbtwnconn1lem3  28596  mideulem2  28756  axlowdimlem16  28986  axcontlem8  29000  vtxval  29031  iedgval  29032  edgval  29080  vtxdgop  29502  finsumvtxdg2size  29582  lp1cycl  30180  ex-ind-dvds  30489  vsfval  30661  lnocoi  30785  nmblolbii  30827  ipasslem5  30863  hvsubid  31054  sshjval3  31382  pjhthlem1  31419  adjval  31918  unopf1o  31944  kbpj  31984  lnopmi  32028  nmcoplbi  32056  cnlnadjlem2  32096  adjadd  32121  branmfn  32133  pjtoi  32207  ofoprabco  32680  supppreima  32705  hashxpe  32816  ccatws1f1o  32920  splfv3  32927  xrsmulgzz  32993  mndractfo  33016  mndlactf1o  33017  mndractf1o  33018  gsumfs2d  33040  psgnfzto1stlem  33102  cycpmco2lem5  33132  cycpmco2lem6  33133  cyc3co2  33142  tocyccntz  33146  cyc3genpmlem  33153  cyc3conja  33159  archiabllem1a  33180  gsumvsca1  33214  gsumvsca2  33215  elrgspnlem2  33232  rloccring  33256  imaslmod  33360  elrspunidl  33435  mxidlirredi  33478  opprabs  33489  qsdrngi  33502  1arithidomlem1  33542  1arithidomlem2  33543  zringfrac  33561  ply1degltdimlem  33649  fedgmullem1  33656  algextdeglem4  33725  constrconj  33749  submat1n  33765  submatres  33766  madjusmdetlem3  33789  xrge0iifhom  33897  qqhval2lem  33943  qqhrhm  33951  qqhucn  33954  esumsnf  34044  measvunilem0  34193  carsgclctunlem1  34298  ballotlemfp1  34472  ballotlemsf1o  34494  signstfveq0  34570  breprexplemc  34625  breprexp  34626  breprexpnat  34627  circlemeth  34633  logdivsqrle  34643  hgt750lema  34650  revwlk  35108  cvmlift3lem2  35304  cvmlift3lem4  35306  cvmlift3lem5  35307  cvmlift3lem6  35308  cvmlift3lem9  35311  elmrsubrn  35504  bccolsum  35718  bj-bary1lem  37292  finixpnum  37591  poimirlem4  37610  poimirlem16  37622  poimirlem19  37625  poimirlem25  37631  mblfinlem3  37645  dvtan  37656  itg2addnc  37660  itgaddnclem2  37665  ftc1anclem6  37684  areacirclem5  37698  areacirc  37699  upixp  37715  prdsbnd2  37781  ismrer1  37824  rngoneglmul  37929  rngoisocnv  37967  islshpsm  38961  lshpnel2N  38966  lfl0f  39050  ldualvsdi1  39124  ldualgrplem  39126  cmtcomlemN  39229  cvlsupr8  39330  pmodl42N  39833  pmapjat1  39835  llnmod2i2  39845  dalawlem2  39854  pmapj2N  39911  idltrn  40132  cdlemc6  40178  cdleme20d  40294  cdleme22e  40326  cdleme22eALTN  40327  cdleme35b  40432  cdleme48fvg  40482  cdlemg4d  40595  cdlemg8a  40609  cdlemg42  40711  cdlemg47a  40716  tendodi1  40766  tendodi2  40767  cdlemk4  40816  cdlemk21N  40855  cdlemk22  40875  cdlemky  40908  cdlemk53b  40938  cdlemk53  40939  cdlemkyyN  40944  erngdvlem3-rN  40980  tendocnv  41003  dia1dim2  41044  dicvaddcl  41172  dihglblem3N  41277  dihmeetlem4preN  41288  dihmeet2  41328  lcfl7lem  41481  baerlem3lem1  41689  baerlem5alem1  41690  mapdh6bN  41719  mapdh6cN  41720  mapdh6dN  41721  hdmap1l6b  41793  hdmap1l6c  41794  hdmap1l6d  41795  hdmap14lem13  41862  ofun  42255  grpcominv1  42494  evlselv  42573  flt4lem7  42645  3cubeslem2  42672  3cubeslem3r  42674  3cubeslem4  42676  pellexlem2  42817  rmxyneg  42908  oddcomabszz  42932  acongeq  42971  hausgraph  43193  onsupnmax  43216  tfsconcatrev  43337  naddass1  43382  fsovrfovd  43998  inductionexd  44144  expgrowth  44330  binomcxplemwb  44343  binomcxplemnn0  44344  binomcxplemnotnn0  44351  sumsnd  44963  restuni4  45060  fmuldfeqlem1  45537  cncfmptss  45542  climexp  45560  dvresntr  45873  stoweidlem17  45972  wallispi  46025  dirkertrigeq  46056  dirkercncflem2  46059  fourierdlem30  46092  fourierdlem41  46103  fourierdlem81  46142  fourierdlem103  46164  sge0xp  46384  sge0isummpt2  46387  isomennd  46486  vonioolem1  46635  sigarperm  46815  fcores  47016  imasetpreimafvbijlemfo  47329  fundcmpsurbijinjpreimafv  47331  fundcmpsurinjimaid  47335  prprspr2  47442  opoeALTV  47607  uhgrimisgrgric  47836  isubgr3stgrlem2  47869  cznrng  48104  rngchomrnghmresALTV  48122  fdmdifeqresdif  48186  lincsum  48274  lincscm  48275  lmod1lem4  48335  blennngt2o2  48441  blennn0e2  48443  topdlat  48792  oppgoppchom  48898  oppgoppcco  48899  oppgoppcid  48900  reccot  48988  rectan  48989  cotsqcscsq  48992  amgmlemALT  49033