Theorem 3eqtr4rd 2809

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  csbun  4402  csbdif  4484  csbcnvgALTOLD  5878  csbres  5989  fimacnvinrn2  7104  f1ossf1o  7161  suppvalbrOLD  8219  odi  8625  phplem2  9258  cantnfp1lem3  9718  cantnfp1  9719  cardidm  10077  ackbij2lem2  10356  ackbij2lem3  10357  divneg  12048  xadddilem  13464  xadddi2  13467  dfceil2  14019  modlt  14060  modmulnn  14069  seqcaopr3  14220  bcval5  14503  hashgadd  14562  hashun3  14569  hashmap  14621  seqcoll  14650  revccat  14957  cshwmodn  14988  2cshwcom  15009  cshimadifsn0  15023  revco  15027  cshco  15029  ofccat  15165  relexpsucl  15227  dfrtrclrec2  15254  cjreb  15333  recj  15334  imcj  15342  imval2  15361  sqrtmul  15469  absmax  15540  amgm2  15581  summolem2a  15925  fsumf1o  15933  sumsnf  15953  sumsplit  15978  fsummulc2  15994  binom  16043  bcxmas  16048  incexclem  16049  incexc  16050  expcnv  16077  pwdif  16081  cvgrat  16096  prodmolem3  16144  prodmolem2a  16145  fprodf1o  16157  prodsn  16173  prodsnf  16175  fprodabs  16185  binomfallfac  16251  fallfacval4  16253  bcfallfac  16254  ege2le3  16300  efaddlem  16303  eftlub  16321  tanval3  16346  tanneg  16360  cosmul  16385  cos01bnd  16398  demoivreALT  16413  flodddiv4  16629  absmulgcd  16766  nn0expgcd  16782  lcmfunsnlem2  16859  eulerthlem2  17003  phisum  17012  pythagtriplem14  17050  pythagtriplem19  17055  pcmul  17073  pcfac  17121  prmreclem6  17143  4sqlem12  17178  vdwlem6  17208  oppccatid  17943  curf2ndf  18471  oppcyon  18493  joincomALT  18623  meetcomALT  18625  pwsco1mhm  19078  sgrp2nmndlem4  19177  qusgrp2  19318  mulgnngsum  19339  mulgnn0p1  19345  mulgneg  19352  mulgnn0dir  19364  qusghm  19519  gaid  19564  symgval  19636  pmtrdifellem3  19743  psgnunilem2  19760  odmulg  19821  sylow1lem2  19864  sylow2a  19884  sylow3lem1  19892  efgredleme  20008  efgcpbllemb  20020  gsumzaddlem  20186  gsumconst  20199  gsumzmhm  20202  ablsimpgfindlem1  20374  srgpcomp  20495  srgbinom  20508  rdivmuldivd  20694  c0mgm  20740  c0mhm  20741  zrrnghm  20839  imadrhmcl  21105  lmodvsmmulgdi  21223  lmodsubdi  21245  rmodislmodlem  21255  0lmhm  21366  lspsneq  21451  qusrhm  21621  quscrng  21630  zringlpirlem3  21825  mulgrhm  21838  phssip  22019  frlmip  22139  frlmphl  22142  asclmulg  22265  resspsrmul  22338  evlsscasrng  22469  psdadd  22539  psdvsca  22540  psdmul  22542  psdpw  22546  psropprmul  22610  evls1scasrng  22712  mat1ghm  22853  mat1mhm  22854  1marepvmarrepid  22945  mdetrlin  22972  mdetrsca2  22974  mdetunilem7  22988  mdetunilem9  22990  mndifsplit  23006  maducoeval2  23010  smadiadetglem2  23042  decpmatmul  23145  pm2mpghm  23189  pm2mpmhmlem2  23192  cpmidgsum2  23252  ptbasfi  23955  ptuni  23968  alexsubALTlem3  24423  subgtgp  24479  tsmsxplem1  24527  xmsusp  24943  restmetu  24944  nminv  24995  nrginvrcnlem  25065  copco  25394  pcoass  25400  pi1bas  25414  pi1xfrf  25429  pi1xfr  25431  isclmp  25473  cph2subdi  25586  cphassr  25588  tcphcphlem1  25611  cphipval  25619  rrxip  25766  rrxnm  25767  pjthlem1  25813  ovolunlem1a  25872  ovolfs2  25947  uniiccdif  25954  ismbf  26004  itgaddlem2  26199  ditgswap  26234  ply1divex  26510  plyeq0lem  26584  plymullem1  26588  dgrcolem1  26647  dgrcolem2  26648  vieta1lem2  26689  elqaalem2  26700  elqaalem3  26701  aaliou3lem7  26733  ulmshft  26774  mulcxplem  27069  cxpmul2  27074  root1eq1  27140  cxpeq  27142  logbchbase  27156  cosangneg2d  27192  isosctrlem2  27204  angpieqvdlem  27213  chordthmlem3  27219  chordthmlem4  27220  chordthmlem5  27221  quad2  27224  dcubic2  27229  cubic2  27233  quart1  27241  scvxcvx  27370  igamlgam  27434  lgam1  27448  basellem9  27473  ppifl  27544  mumul  27565  sgmmul  27585  chtublem  27595  chpub  27604  logfacrlim  27608  dchrsum2  27652  sumdchr2  27654  bposlem9  27676  lgsdir2  27714  lgsdir  27716  lgsdi  27718  lgsdirnn0  27728  lgsdinn0  27729  lgsquad3  27771  2sqblem  27815  chpo1ub  27864  dchrmusum2  27878  dchrvmasumlem1  27879  dchrvmasum2if  27881  dchrisum0fmul  27890  rpvmasum2  27896  mulog2sumlem1  27918  vmalogdivsum2  27922  log2sumbnd  27928  selberg3lem1  27941  selberg4lem1  27944  pntrsumo1  27949  selbergr  27952  pntpbnd1  27970  pntlemk  27990  flt4lem7  28046  lesubsd  28539  mulsunif2lem  28612  divsasswd  28646  absmuls  28687  eucliddivs  28819  zcuts  28850  expsp1  28872  expadds  28878  pw2divsrecd  28890  pw2cut2  28905  bdayfinbndlem1  28910  tgbtwnconn1lem3  29094  mideulem2  29267  axlowdimlem16  29592  axcontlem8  29606  vtxval  29635  iedgval  29636  edgval  29684  vtxdgop  30108  finsumvtxdg2size  30188  revwlk  30324  lp1cycl  30800  ex-ind-dvds  31119  vsfval  31292  lnocoi  31416  nmblolbii  31458  ipasslem5  31494  hvsubid  31685  sshjval3  32013  pjhthlem1  32050  adjval  32549  unopf1o  32575  kbpj  32615  lnopmi  32659  nmcoplbi  32687  cnlnadjlem2  32727  adjadd  32752  branmfn  32764  pjtoi  32838  fconst7v  33312  ofoprabco  33356  supppreima  33381  sgnval2  33423  hashxpe  33495  ccatws1f1o  33610  splfv3  33615  xrsmulgzz  33669  mndractfo  33689  mndlactf1o  33690  mndractf1o  33691  gsumfs2d  33721  psgnfzto1stlem  33760  cycpmco2lem5  33790  cycpmco2lem6  33791  cyc3co2  33800  tocyccntz  33804  cyc3genpmlem  33811  cyc3conja  33817  archiabllem1a  33851  gsumvsca1  33886  gsumvsca2  33887  elrgspnlem2  33903  elrgspnsubrunlem1  33907  rloccring  33931  imaslmod  34018  elrspunidl  34082  mxidlirredi  34100  opprabs  34110  qsdrngi  34123  1arithidomlem1  34171  1arithidomlem2  34172  zringfrac  34189  ressply1evls1  34200  deg1prod  34218  evls1degle1  34239  rngunsnply1chr2lem3  34252  psrbasfsupp  34254  selvply1rhmlem4  34266  mplvrpmga  34288  esplyind  34318  vietalem  34322  vieta  34323  ply1degltdimlem  34365  fedgmullem1  34372  fldextrspunlsplem  34416  extdgfialglem2  34436  algextdeglem4  34463  constrconj  34488  constrdircl  34508  constrremulcl  34510  constrimcl  34513  constrresqrtcl  34520  cos9thpiminplylem2  34526  submat1n  34548  submatres  34549  madjusmdetlem3  34572  xrge0iifhom  34680  qqhval2lem  34724  qqhrhm  34732  qqhucn  34735  esumsnf  34807  measvunilem0  34957  carsgclctunlem1  35060  ballotlemfp1  35235  ballotlemsf1o  35257  signstfveq0  35317  breprexplemc  35372  breprexp  35373  breprexpnat  35374  circlemeth  35380  logdivsqrle  35390  hgt750lema  35397  gdlopcfv5  36017  gdlopcfv6  36018  gdlopcfv7  36019  gdlopcfv8  36020  cvmlift3lem2  36293  cvmlift3lem4  36295  cvmlift3lem5  36296  cvmlift3lem6  36297  cvmlift3lem9  36300  elmrsubrn  36493  bccolsum  36719  bj-bary1lem  38499  qdiff  38516  finixpnum  38796  poimirlem4  38810  poimirlem16  38822  poimirlem19  38825  poimirlem25  38831  mblfinlem3  38845  dvtan  38856  itg2addnc  38860  itgaddnclem2  38865  ftc1anclem6  38884  areacirclem5  38898  areacirc  38899  upixp  38931  prdsbnd2  38995  ismrer1  39038  rngoneglmul  39143  rngoisocnv  39181  ecun  39591  islshpsm  40303  lshpnel2N  40308  lfl0f  40392  ldualvsdi1  40466  ldualgrplem  40468  cmtcomlemN  40571  cvlsupr8  40672  pmodl42N  41174  pmapjat1  41176  llnmod2i2  41186  dalawlem2  41195  pmapj2N  41252  idltrn  41473  cdlemc6  41519  cdleme20d  41635  cdleme22e  41667  cdleme22eALTN  41668  cdleme35b  41773  cdleme48fvg  41823  cdlemg4d  41936  cdlemg8a  41950  cdlemg42  42052  cdlemg47a  42057  tendodi1  42107  tendodi2  42108  cdlemk4  42157  cdlemk21N  42196  cdlemk22  42216  cdlemky  42249  cdlemk53b  42279  cdlemk53  42280  cdlemkyyN  42285  erngdvlem3-rN  42321  tendocnv  42344  dia1dim2  42385  dicvaddcl  42513  dihglblem3N  42618  dihmeetlem4preN  42629  dihmeet2  42669  lcfl7lem  42822  baerlem3lem1  43030  baerlem5alem1  43031  mapdh6bN  43060  mapdh6cN  43061  mapdh6dN  43062  hdmap1l6b  43134  hdmap1l6c  43135  hdmap1l6d  43136  hdmap14lem13  43203  ofun  43556  rediv23d  43778  grpcominv1  43841  evlselv  43883  3cubeslem2  43961  3cubeslem3r  43963  3cubeslem4  43965  pellexlem2  44103  rmxyneg  44193  oddcomabszz  44217  acongeq  44256  hausgraph  44468  onsupnmax  44491  tfsconcatrev  44611  naddass1  44656  fsovrfovd  45270  inductionexd  45416  expgrowth  45580  binomcxplemwb  45593  binomcxplemnn0  45594  binomcxplemnotnn0  45601  sumsnd  46317  restuni4  46409  fmuldfeqlem1  46867  cncfmptss  46872  climexp  46890  dvresntr  47201  stoweidlem17  47300  wallispi  47353  dirkertrigeq  47384  dirkercncflem2  47387  fourierdlem30  47420  fourierdlem41  47431  fourierdlem81  47470  fourierdlem103  47492  sge0xp  47712  sge0isummpt2  47715  isomennd  47814  vonioolem1  47963  sigarperm  48143  sin3t  48190  sin5tlem5  48196  fcores  48410  imasetpreimafvbijlemfo  48760  fundcmpsurbijinjpreimafv  48762  fundcmpsurinjimaid  48766  prprspr2  48873  ppivalnn  48990  opoeALTV  49054  uhgrimisgrgric  49302  isubgr3stgrlem2  49338  cznrng  49631  rngchomrnghmresALTV  49649  fdmdifeqresdif  49785  lincsum  49872  lincscm  49873  lmod1lem4  49933  blennngt2o2  50035  blennn0e2  50037  tposideq  50332  topdlat  50449  sectpropdlem  50481  invpropdlem  50483  isopropdlem  50485  imaidfu  50557  imasubc  50598  natoppf  50682  swapfid  50732  swapfcoa  50734  fucoppcid  50874  fucoppcco  50875  oppfdiag1  50880  diag1f1olem  50999  oppgoppchom  51059  oppgoppcco  51060  oppgoppcid  51061  2arwcat  51069  parmapco2  51103  parmapco  51104  parmapfunc2  51105  sinhneg  51242  tanhneg  51252  tanhadd  51258  reccot  51279  rectan  51280  cotsqcscsq  51283  crosspaltd  51394  crossp3d  51395  amgmlemALT  51416