Theorem 3eqtr4rd 2783

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  csbun  4382  csbdif  4466  csbcnvgALT  5834  csbres  5942  fimacnvinrn2  7019  f1ossf1o  7076  suppvalbr  8108  odi  8508  phplem2  9133  cantnfp1lem3  9595  cantnfp1  9596  cardidm  9877  ackbij2lem2  10155  ackbij2lem3  10156  divneg  11840  xadddilem  13240  xadddi2  13243  dfceil2  13792  modlt  13833  modmulnn  13842  seqcaopr3  13993  bcval5  14274  hashgadd  14333  hashun3  14340  hashmap  14391  seqcoll  14420  revccat  14722  cshwmodn  14751  2cshwcom  14772  cshimadifsn0  14786  revco  14790  cshco  14792  ofccat  14925  relexpsucl  14987  dfrtrclrec2  15014  cjreb  15079  recj  15080  imcj  15088  imval2  15107  sqrtmul  15215  absmax  15286  amgm2  15326  summolem2a  15671  fsumf1o  15679  sumsnf  15699  sumsplit  15724  fsummulc2  15740  binom  15789  bcxmas  15794  incexclem  15795  incexc  15796  expcnv  15823  pwdif  15827  cvgrat  15842  prodmolem3  15892  prodmolem2a  15893  fprodf1o  15905  prodsn  15921  prodsnf  15923  fprodabs  15933  binomfallfac  16000  fallfacval4  16002  bcfallfac  16003  ege2le3  16049  efaddlem  16052  eftlub  16070  tanval3  16095  tanneg  16109  cosmul  16134  cos01bnd  16147  demoivreALT  16162  flodddiv4  16378  absmulgcd  16512  nn0expgcd  16527  lcmfunsnlem2  16603  eulerthlem2  16746  phisum  16755  pythagtriplem14  16793  pythagtriplem19  16798  pcmul  16816  pcfac  16864  prmreclem6  16886  4sqlem12  16921  vdwlem6  16951  oppccatid  17679  curf2ndf  18207  oppcyon  18229  joincomALT  18359  meetcomALT  18361  pwsco1mhm  18794  sgrp2nmndlem4  18893  qusgrp2  19028  mulgnngsum  19049  mulgnn0p1  19055  mulgneg  19062  mulgnn0dir  19074  qusghm  19224  gaid  19268  symgval  19340  pmtrdifellem3  19447  psgnunilem2  19464  odmulg  19525  sylow1lem2  19568  sylow2a  19588  sylow3lem1  19596  efgredleme  19712  efgcpbllemb  19724  gsumzaddlem  19890  gsumconst  19903  gsumzmhm  19906  ablsimpgfindlem1  20078  srgpcomp  20193  srgbinom  20206  rdivmuldivd  20387  c0mgm  20433  c0mhm  20434  zrrnghm  20507  imadrhmcl  20768  lmodvsmmulgdi  20886  lmodsubdi  20908  rmodislmodlem  20918  0lmhm  21030  lspsneq  21115  qusrhm  21269  quscrng  21276  zringlpirlem3  21457  mulgrhm  21470  phssip  21651  frlmip  21771  frlmphl  21774  asclmulg  21895  resspsrmul  21967  evlsscasrng  22096  psdadd  22142  psdvsca  22143  psdmul  22145  psdpw  22149  psropprmul  22214  evls1scasrng  22317  mat1ghm  22461  mat1mhm  22462  1marepvmarrepid  22553  mdetrlin  22580  mdetrsca2  22582  mdetunilem7  22596  mdetunilem9  22598  mndifsplit  22614  maducoeval2  22618  smadiadetglem2  22650  decpmatmul  22750  pm2mpghm  22794  pm2mpmhmlem2  22797  cpmidgsum2  22857  ptbasfi  23559  ptuni  23572  alexsubALTlem3  24027  subgtgp  24083  tsmsxplem1  24131  xmsusp  24547  restmetu  24548  nminv  24599  nrginvrcnlem  24669  copco  24998  pcoass  25004  pi1bas  25018  pi1xfrf  25033  pi1xfr  25035  isclmp  25077  cph2subdi  25190  cphassr  25192  tcphcphlem1  25215  cphipval  25223  rrxip  25370  rrxnm  25371  pjthlem1  25417  ovolunlem1a  25476  ovolfs2  25551  uniiccdif  25558  ismbf  25608  itgaddlem2  25804  ditgswap  25839  ply1divex  26115  plyeq0lem  26188  plymullem1  26192  dgrcolem1  26251  dgrcolem2  26252  vieta1lem2  26291  elqaalem2  26300  elqaalem3  26301  aaliou3lem7  26329  ulmshft  26371  mulcxplem  26664  cxpmul2  26669  root1eq1  26735  cxpeq  26737  logbchbase  26751  cosangneg2d  26787  isosctrlem2  26799  angpieqvdlem  26808  chordthmlem3  26814  chordthmlem4  26815  chordthmlem5  26816  quad2  26819  dcubic2  26824  cubic2  26828  quart1  26836  scvxcvx  26966  igamlgam  27030  lgam1  27044  basellem9  27069  ppifl  27140  mumul  27161  sgmmul  27181  chtublem  27191  chpub  27200  logfacrlim  27204  dchrsum2  27248  sumdchr2  27250  bposlem9  27272  lgsdir2  27310  lgsdir  27312  lgsdi  27314  lgsdirnn0  27324  lgsdinn0  27325  lgsquad3  27367  2sqblem  27411  chpo1ub  27460  dchrmusum2  27474  dchrvmasumlem1  27475  dchrvmasum2if  27477  dchrisum0fmul  27486  rpvmasum2  27492  mulog2sumlem1  27514  vmalogdivsum2  27518  log2sumbnd  27524  selberg3lem1  27537  selberg4lem1  27540  pntrsumo1  27545  selbergr  27548  pntpbnd1  27566  pntlemk  27586  lesubsd  28105  mulsunif2lem  28178  divsasswd  28212  absmuls  28253  eucliddivs  28385  zcuts  28416  expsp1  28438  expadds  28444  pw2divsrecd  28456  pw2cut2  28471  bdayfinbndlem1  28476  tgbtwnconn1lem3  28659  mideulem2  28819  axlowdimlem16  29043  axcontlem8  29057  vtxval  29086  iedgval  29087  edgval  29135  vtxdgop  29557  finsumvtxdg2size  29637  lp1cycl  30240  ex-ind-dvds  30549  vsfval  30722  lnocoi  30846  nmblolbii  30888  ipasslem5  30924  hvsubid  31115  sshjval3  31443  pjhthlem1  31480  adjval  31979  unopf1o  32005  kbpj  32045  lnopmi  32089  nmcoplbi  32117  cnlnadjlem2  32157  adjadd  32182  branmfn  32194  pjtoi  32268  fconst7v  32711  ofoprabco  32755  supppreima  32782  sgnval2  32826  hashxpe  32898  ccatws1f1o  33029  splfv3  33036  xrsmulgzz  33087  mndractfo  33107  mndlactf1o  33108  mndractf1o  33109  gsumfs2d  33140  psgnfzto1stlem  33179  cycpmco2lem5  33209  cycpmco2lem6  33210  cyc3co2  33219  tocyccntz  33223  cyc3genpmlem  33230  cyc3conja  33236  archiabllem1a  33270  gsumvsca1  33305  gsumvsca2  33306  elrgspnlem2  33322  elrgspnsubrunlem1  33326  rloccring  33349  imaslmod  33431  elrspunidl  33506  mxidlirredi  33549  opprabs  33560  qsdrngi  33573  1arithidomlem1  33613  1arithidomlem2  33614  zringfrac  33632  ressply1evls1  33643  deg1prod  33661  psrbasfsupp  33690  mplvrpmga  33707  esplyind  33737  vietalem  33741  vieta  33742  ply1degltdimlem  33785  fedgmullem1  33792  fldextrspunlsplem  33836  extdgfialglem2  33856  algextdeglem4  33883  constrconj  33908  constrdircl  33928  constrremulcl  33930  constrimcl  33933  constrresqrtcl  33940  cos9thpiminplylem2  33946  submat1n  33968  submatres  33969  madjusmdetlem3  33992  xrge0iifhom  34100  qqhval2lem  34144  qqhrhm  34152  qqhucn  34155  esumsnf  34227  measvunilem0  34376  carsgclctunlem1  34480  ballotlemfp1  34655  ballotlemsf1o  34677  signstfveq0  34740  breprexplemc  34795  breprexp  34796  breprexpnat  34797  circlemeth  34803  logdivsqrle  34813  hgt750lema  34820  revwlk  35326  cvmlift3lem2  35521  cvmlift3lem4  35523  cvmlift3lem5  35524  cvmlift3lem6  35525  cvmlift3lem9  35528  elmrsubrn  35721  bccolsum  35940  bj-bary1lem  37643  finixpnum  37943  poimirlem4  37962  poimirlem16  37974  poimirlem19  37977  poimirlem25  37983  mblfinlem3  37997  dvtan  38008  itg2addnc  38012  itgaddnclem2  38017  ftc1anclem6  38036  areacirclem5  38050  areacirc  38051  upixp  38067  prdsbnd2  38133  ismrer1  38176  rngoneglmul  38281  rngoisocnv  38319  ecun  38731  islshpsm  39443  lshpnel2N  39448  lfl0f  39532  ldualvsdi1  39606  ldualgrplem  39608  cmtcomlemN  39711  cvlsupr8  39812  pmodl42N  40314  pmapjat1  40316  llnmod2i2  40326  dalawlem2  40335  pmapj2N  40392  idltrn  40613  cdlemc6  40659  cdleme20d  40775  cdleme22e  40807  cdleme22eALTN  40808  cdleme35b  40913  cdleme48fvg  40963  cdlemg4d  41076  cdlemg8a  41090  cdlemg42  41192  cdlemg47a  41197  tendodi1  41247  tendodi2  41248  cdlemk4  41297  cdlemk21N  41336  cdlemk22  41356  cdlemky  41389  cdlemk53b  41419  cdlemk53  41420  cdlemkyyN  41425  erngdvlem3-rN  41461  tendocnv  41484  dia1dim2  41525  dicvaddcl  41653  dihglblem3N  41758  dihmeetlem4preN  41769  dihmeet2  41809  lcfl7lem  41962  baerlem3lem1  42170  baerlem5alem1  42171  mapdh6bN  42200  mapdh6cN  42201  mapdh6dN  42202  hdmap1l6b  42274  hdmap1l6c  42275  hdmap1l6d  42276  hdmap14lem13  42343  ofun  42694  rediv23d  42910  grpcominv1  42970  evlselv  43037  flt4lem7  43109  3cubeslem2  43134  3cubeslem3r  43136  3cubeslem4  43138  pellexlem2  43279  rmxyneg  43369  oddcomabszz  43393  acongeq  43432  hausgraph  43654  onsupnmax  43677  tfsconcatrev  43797  naddass1  43842  fsovrfovd  44457  inductionexd  44603  expgrowth  44783  binomcxplemwb  44796  binomcxplemnn0  44797  binomcxplemnotnn0  44804  sumsnd  45478  restuni4  45572  fmuldfeqlem1  46033  cncfmptss  46038  climexp  46056  dvresntr  46367  stoweidlem17  46466  wallispi  46519  dirkertrigeq  46550  dirkercncflem2  46553  fourierdlem30  46586  fourierdlem41  46597  fourierdlem81  46636  fourierdlem103  46658  sge0xp  46878  sge0isummpt2  46881  isomennd  46980  vonioolem1  47129  sigarperm  47309  sin3t  47338  sin5tlem5  47344  fcores  47530  imasetpreimafvbijlemfo  47880  fundcmpsurbijinjpreimafv  47882  fundcmpsurinjimaid  47886  prprspr2  47993  ppivalnn  48110  opoeALTV  48174  uhgrimisgrgric  48422  isubgr3stgrlem2  48458  cznrng  48752  rngchomrnghmresALTV  48770  fdmdifeqresdif  48833  lincsum  48920  lincscm  48921  lmod1lem4  48981  blennngt2o2  49083  blennn0e2  49085  tposideq  49378  topdlat  49494  sectpropdlem  49526  invpropdlem  49528  isopropdlem  49530  imaidfu  49600  imasubc  49641  natoppf  49719  swapfid  49769  swapfcoa  49771  fucoppcid  49898  fucoppcco  49899  oppfdiag1  49904  diag1f1olem  50023  oppgoppchom  50080  oppgoppcco  50081  oppgoppcid  50082  2arwcat  50090  reccot  50248  rectan  50249  cotsqcscsq  50252  amgmlemALT  50293