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 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  csbun  4369  csbdif  4453  csbcnvgALT  5826  csbres  5934  fimacnvinrn2  7013  f1ossf1o  7070  suppvalbr  8104  odi  8504  phplem2  9129  cantnfp1lem3  9592  cantnfp1  9593  cardidm  9874  ackbij2lem2  10152  ackbij2lem3  10153  divneg  11837  xadddilem  13237  xadddi2  13240  dfceil2  13789  modlt  13830  modmulnn  13839  seqcaopr3  13990  bcval5  14271  hashgadd  14330  hashun3  14337  hashmap  14388  seqcoll  14417  revccat  14719  cshwmodn  14748  2cshwcom  14769  cshimadifsn0  14783  revco  14787  cshco  14789  ofccat  14922  relexpsucl  14984  dfrtrclrec2  15011  cjreb  15076  recj  15077  imcj  15085  imval2  15104  sqrtmul  15212  absmax  15283  amgm2  15323  summolem2a  15668  fsumf1o  15676  sumsnf  15696  sumsplit  15721  fsummulc2  15737  binom  15786  bcxmas  15791  incexclem  15792  incexc  15793  expcnv  15820  pwdif  15824  cvgrat  15839  prodmolem3  15889  prodmolem2a  15890  fprodf1o  15902  prodsn  15918  prodsnf  15920  fprodabs  15930  binomfallfac  15997  fallfacval4  15999  bcfallfac  16000  ege2le3  16046  efaddlem  16049  eftlub  16067  tanval3  16092  tanneg  16106  cosmul  16131  cos01bnd  16144  demoivreALT  16159  flodddiv4  16375  absmulgcd  16509  nn0expgcd  16524  lcmfunsnlem2  16600  eulerthlem2  16743  phisum  16752  pythagtriplem14  16790  pythagtriplem19  16795  pcmul  16813  pcfac  16861  prmreclem6  16883  4sqlem12  16918  vdwlem6  16948  oppccatid  17676  curf2ndf  18204  oppcyon  18226  joincomALT  18356  meetcomALT  18358  pwsco1mhm  18791  sgrp2nmndlem4  18890  qusgrp2  19025  mulgnngsum  19046  mulgnn0p1  19052  mulgneg  19059  mulgnn0dir  19071  qusghm  19221  gaid  19265  symgval  19337  pmtrdifellem3  19444  psgnunilem2  19461  odmulg  19522  sylow1lem2  19565  sylow2a  19585  sylow3lem1  19593  efgredleme  19709  efgcpbllemb  19721  gsumzaddlem  19887  gsumconst  19900  gsumzmhm  19903  ablsimpgfindlem1  20075  srgpcomp  20190  srgbinom  20203  rdivmuldivd  20384  c0mgm  20430  c0mhm  20431  zrrnghm  20508  imadrhmcl  20769  lmodvsmmulgdi  20887  lmodsubdi  20909  rmodislmodlem  20919  0lmhm  21030  lspsneq  21115  qusrhm  21269  quscrng  21276  zringlpirlem3  21439  mulgrhm  21452  phssip  21633  frlmip  21753  frlmphl  21756  asclmulg  21877  resspsrmul  21950  evlsscasrng  22081  psdadd  22151  psdvsca  22152  psdmul  22154  psdpw  22158  psropprmul  22222  evls1scasrng  22325  mat1ghm  22466  mat1mhm  22467  1marepvmarrepid  22558  mdetrlin  22585  mdetrsca2  22587  mdetunilem7  22601  mdetunilem9  22603  mndifsplit  22619  maducoeval2  22623  smadiadetglem2  22655  decpmatmul  22755  pm2mpghm  22799  pm2mpmhmlem2  22802  cpmidgsum2  22862  ptbasfi  23564  ptuni  23577  alexsubALTlem3  24032  subgtgp  24088  tsmsxplem1  24136  xmsusp  24552  restmetu  24553  nminv  24604  nrginvrcnlem  24674  copco  25003  pcoass  25009  pi1bas  25023  pi1xfrf  25038  pi1xfr  25040  isclmp  25082  cph2subdi  25195  cphassr  25197  tcphcphlem1  25220  cphipval  25228  rrxip  25375  rrxnm  25376  pjthlem1  25422  ovolunlem1a  25481  ovolfs2  25556  uniiccdif  25563  ismbf  25613  itgaddlem2  25809  ditgswap  25844  ply1divex  26120  plyeq0lem  26193  plymullem1  26197  dgrcolem1  26256  dgrcolem2  26257  vieta1lem2  26295  elqaalem2  26304  elqaalem3  26305  aaliou3lem7  26333  ulmshft  26373  mulcxplem  26666  cxpmul2  26671  root1eq1  26737  cxpeq  26739  logbchbase  26753  cosangneg2d  26789  isosctrlem2  26801  angpieqvdlem  26810  chordthmlem3  26816  chordthmlem4  26817  chordthmlem5  26818  quad2  26821  dcubic2  26826  cubic2  26830  quart1  26838  scvxcvx  26967  igamlgam  27031  lgam1  27045  basellem9  27070  ppifl  27141  mumul  27162  sgmmul  27182  chtublem  27192  chpub  27201  logfacrlim  27205  dchrsum2  27249  sumdchr2  27251  bposlem9  27273  lgsdir2  27311  lgsdir  27313  lgsdi  27315  lgsdirnn0  27325  lgsdinn0  27326  lgsquad3  27368  2sqblem  27412  chpo1ub  27461  dchrmusum2  27475  dchrvmasumlem1  27476  dchrvmasum2if  27478  dchrisum0fmul  27487  rpvmasum2  27493  mulog2sumlem1  27515  vmalogdivsum2  27519  log2sumbnd  27525  selberg3lem1  27538  selberg4lem1  27541  pntrsumo1  27546  selbergr  27549  pntpbnd1  27567  pntlemk  27587  lesubsd  28106  mulsunif2lem  28179  divsasswd  28213  absmuls  28254  eucliddivs  28386  zcuts  28417  expsp1  28439  expadds  28445  pw2divsrecd  28457  pw2cut2  28472  bdayfinbndlem1  28477  tgbtwnconn1lem3  28660  mideulem2  28820  axlowdimlem16  29044  axcontlem8  29058  vtxval  29087  iedgval  29088  edgval  29136  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  32712  ofoprabco  32756  supppreima  32783  sgnval2  32827  hashxpe  32899  ccatws1f1o  33030  splfv3  33037  xrsmulgzz  33088  mndractfo  33108  mndlactf1o  33109  mndractf1o  33110  gsumfs2d  33142  psgnfzto1stlem  33181  cycpmco2lem5  33211  cycpmco2lem6  33212  cyc3co2  33221  tocyccntz  33225  cyc3genpmlem  33232  cyc3conja  33238  archiabllem1a  33272  gsumvsca1  33307  gsumvsca2  33308  elrgspnlem2  33324  elrgspnsubrunlem1  33328  rloccring  33351  imaslmod  33436  elrspunidl  33511  mxidlirredi  33554  opprabs  33565  qsdrngi  33578  1arithidomlem1  33618  1arithidomlem2  33619  zringfrac  33637  ressply1evls1  33648  deg1prod  33666  psrbasfsupp  33695  selvply1rhmlem4  33707  mplvrpmga  33729  esplyind  33759  vietalem  33763  vieta  33764  ply1degltdimlem  33806  fedgmullem1  33813  fldextrspunlsplem  33857  extdgfialglem2  33877  algextdeglem4  33904  constrconj  33929  constrdircl  33949  constrremulcl  33951  constrimcl  33954  constrresqrtcl  33961  cos9thpiminplylem2  33967  submat1n  33989  submatres  33990  madjusmdetlem3  34013  xrge0iifhom  34121  qqhval2lem  34165  qqhrhm  34173  qqhucn  34176  esumsnf  34248  measvunilem0  34397  carsgclctunlem1  34501  ballotlemfp1  34676  ballotlemsf1o  34698  signstfveq0  34761  breprexplemc  34816  breprexp  34817  breprexpnat  34818  circlemeth  34824  logdivsqrle  34834  hgt750lema  34841  revwlk  35353  cvmlift3lem2  35548  cvmlift3lem4  35550  cvmlift3lem5  35551  cvmlift3lem6  35552  cvmlift3lem9  35555  elmrsubrn  35748  bccolsum  35967  bj-bary1lem  37670  qdiff  37687  finixpnum  37972  poimirlem4  37991  poimirlem16  38003  poimirlem19  38006  poimirlem25  38012  mblfinlem3  38026  dvtan  38037  itg2addnc  38041  itgaddnclem2  38046  ftc1anclem6  38065  areacirclem5  38079  areacirc  38080  upixp  38096  prdsbnd2  38162  ismrer1  38205  rngoneglmul  38310  rngoisocnv  38348  ecun  38760  islshpsm  39472  lshpnel2N  39477  lfl0f  39561  ldualvsdi1  39635  ldualgrplem  39637  cmtcomlemN  39740  cvlsupr8  39841  pmodl42N  40343  pmapjat1  40345  llnmod2i2  40355  dalawlem2  40364  pmapj2N  40421  idltrn  40642  cdlemc6  40688  cdleme20d  40804  cdleme22e  40836  cdleme22eALTN  40837  cdleme35b  40942  cdleme48fvg  40992  cdlemg4d  41105  cdlemg8a  41119  cdlemg42  41221  cdlemg47a  41226  tendodi1  41276  tendodi2  41277  cdlemk4  41326  cdlemk21N  41365  cdlemk22  41385  cdlemky  41418  cdlemk53b  41448  cdlemk53  41449  cdlemkyyN  41454  erngdvlem3-rN  41490  tendocnv  41513  dia1dim2  41554  dicvaddcl  41682  dihglblem3N  41787  dihmeetlem4preN  41798  dihmeet2  41838  lcfl7lem  41991  baerlem3lem1  42199  baerlem5alem1  42200  mapdh6bN  42229  mapdh6cN  42230  mapdh6dN  42231  hdmap1l6b  42303  hdmap1l6c  42304  hdmap1l6d  42305  hdmap14lem13  42372  ofun  42722  rediv23d  42938  grpcominv1  42998  evlselv  43039  flt4lem7  43109  3cubeslem2  43134  3cubeslem3r  43136  3cubeslem4  43138  pellexlem2  43275  rmxyneg  43365  oddcomabszz  43389  acongeq  43428  hausgraph  43650  onsupnmax  43673  tfsconcatrev  43793  naddass1  43838  fsovrfovd  44453  inductionexd  44599  expgrowth  44779  binomcxplemwb  44792  binomcxplemnn0  44793  binomcxplemnotnn0  44800  sumsnd  45474  restuni4  45568  fmuldfeqlem1  46027  cncfmptss  46032  climexp  46050  dvresntr  46361  stoweidlem17  46460  wallispi  46513  dirkertrigeq  46544  dirkercncflem2  46547  fourierdlem30  46580  fourierdlem41  46591  fourierdlem81  46630  fourierdlem103  46652  sge0xp  46872  sge0isummpt2  46875  isomennd  46974  vonioolem1  47123  sigarperm  47303  sin3t  47334  sin5tlem5  47340  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