Theorem 3eqtr2d 2804

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr2d.2	⊢ (𝜑 → 𝐶 = 𝐵)
3eqtr2d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtr2d	⊢ (𝜑 → 𝐴 = 𝐷)

Proof of Theorem 3eqtr2d

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	1, 2	eqtr4d 2801	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2798	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  fmptapd  7171  scottrankd  9875  negsub  11507  neg2sub  11519  divmuleq  11921  divneg2  11940  nnadddir  12293  discr  14278  bcpasc  14359  hashgval2  14416  hashf1lem2  14495  relexpaddnn  15090  crim  15168  remullem  15181  isum1p  15897  geo2sum  15929  fallfacfwd  16091  fsumkthpow  16111  bpoly3  16113  bpoly4  16114  efi4p  16194  sinhval  16211  addcos  16231  cos2tsin  16236  demoivreALT  16258  rpnnen2lem11  16281  omeo  16425  pwp1fsum  16450  sadaddlem  16525  bitsres  16532  smumullem  16551  sqgcd  16621  expgcd  16622  eulerthlem2  16842  vfermltlALT  16863  pockthlem  16966  4sqlem10  17008  vdwlem2  17043  vdwlem6  17047  vdwlem8  17049  fuccocl  18025  resssetc  18150  resscatc  18167  uncfcurf  18296  yonedalem3b  18336  prdspjmhm  18889  grpinvid2  19060  imasgrp2  19122  mulgaddcomlem  19164  mulgmodid  19180  lagsubg2  19266  cntzsgrpcl  19405  cntzsubm  19409  sylow3lem2  19699  efgredleme  19814  ablsubsub  19888  ablsubsub4  19889  odadd2  19920  gex2abl  19922  pgpfac1lem3a  20149  pwspjmhmmgpd  20410  rngcid  20721  ringcid  20750  abvneg  20910  lmodfopne  21002  lsppr  21195  rngqiprngfulem4  21435  gzrngunit  21564  frlmsubgval  21896  frlmgsum  21903  psrass1  22094  resspsradd  22105  resspsrvsca  22107  mplcoe5  22172  mplmon2mul  22201  evlslem2  22211  evlsvarsrng  22239  selvvvval  22274  coe1tm  22415  ply1fermltlchr  22453  evls1varsrng  22481  mamuass  22540  mavmulass  22687  mulmarep1gsum2  22712  mdetuni0  22759  maducoeval2  22778  madulid  22783  mat2pmatmul  22869  decpmatmulsumfsupp  22911  pmatcollpwlem  22918  pm2mpmhmlem1  22956  cmpfi  23546  cnconn  23560  txrest  23769  utopsnneiplem  24385  blcvx  24936  tcphcphlem2  25376  cphipval2  25381  cphipval  25383  rrx0  25537  minveclem2  25566  pjthlem1  25577  uniioovol  25719  uniioombllem2  25723  itg1addlem4  25839  mbfi1fseqlem5  25859  itg2mulc  25887  itg2monolem1  25890  itgaddlem1  25963  itgmulc2lem2  25973  dvrec  26095  lhop2  26155  ftc1lem5  26180  deg1submon1p  26291  plypf1  26350  coefv0  26386  coemulhi  26392  coemulc  26393  dgreq0  26403  dvply1  26426  vieta1  26454  aareccl  26470  aaliou3lem8  26489  dvtaylp  26514  mtest  26548  sineq0  26670  efif1olem2  26689  efif1olem4  26691  tanarg  26765  logtayl2  26808  nnlogbexp  26927  isosctrlem2  26965  chordthmlem2  26979  chordthmlem4  26981  heron  26984  dcubic1lem  26989  dcubic1  26991  mcubic  26993  dquart  26999  quart1lem  27001  quart1  27002  efiasin  27034  asinsin  27038  atancj  27056  efiatan  27058  atanlogaddlem  27059  cosatan  27067  atantan  27069  atans2  27077  log2cnv  27090  log2tlbnd  27091  birthdaylem2  27098  cxplim  27117  lgamgulmlem2  27175  wilthlem1  27213  basellem3  27228  musum  27336  musumsum  27337  muinv  27338  pclogsum  27360  mersenne  27372  dchrabs  27405  dchrinv  27406  lgseisenlem1  27520  lgsquadlem1  27525  lgsquadlem2  27526  lgsquadlem3  27527  lgsquad2lem1  27529  2lgslem1  27539  2sqmod  27581  chebbnd1lem3  27616  chpchtlim  27624  rplogsumlem2  27630  dchrisumlem2  27635  dchrmusum2  27639  mulog2sumlem1  27679  mulog2sumlem3  27681  vmalogdivsum2  27683  selberg4lem1  27705  pntrlog2bndlem2  27723  pntrlog2bndlem4  27725  pntibndlem2  27736  pntlemr  27747  pntlemf  27750  pntlemo  27752  addsdilem4  28328  mulsunif2lem  28343  halfcut  28632  bdayfinbndlem1  28641  ragcom  28959  colperpexlem1  28992  plngrotlem2  29051  plng3p  29060  lmiisolem  29086  hypcgrlem2  29091  trgcopyeulem  29097  brbtwn2  29236  colinearalglem1  29237  colinearalglem2  29238  axcontlem2  29296  axcontlem8  29302  numedglnl  29475  clwlkclwwlklem2a  30330  numclwlk1lem1  30701  numclwlk1lem2  30702  numclwwlk2  30713  grpoinvid2  30862  ablodivdiv4  30887  smcnlem  31030  ipidsq  31043  ipasslem2  31165  minvecolem2  31208  hv2times  31394  pjhthlem1  31724  pjds3i  32046  ho2times  32152  opsqrlem6  32478  pjclem4  32532  pj3si  32540  csmdsymi  32667  ofoprabco  32990  fcnvgreu  32998  quad3d  33075  nn0diffz0  33120  swrdrndisj  33258  trsp2cyc  33424  cycpmco2lem3  33429  cycpmco2lem4  33430  cycpmco2lem5  33431  cycpmco2lem6  33432  cycpmco2  33434  conjga  33471  elrgspnlem1  33543  rlocmulval  33571  rlocinvunit  33576  rlocisunit  33577  imaslmod  33654  1arithufdlem3  33817  deg1prod  33854  r1padd1  33879  selvply1rhmlem2  33892  mplvrpmrhm  33918  esplyfvaln  33945  frlmdim  33982  rrxdim  33985  lbsdiflsp0  33997  fedgmullem1  34000  fedgmullem2  34001  extdg1id  34037  ccfldextdgrr  34043  fldextrspunlem1  34046  constrrtlc1  34103  constrrtcclem  34105  constrrtcc  34106  constrrecl  34140  constrresqrtcl  34148  cos9thpiminplylem1  34153  cos9thpiminplylem2  34154  cos9thpiminplylem3  34155  cos9thpiminply  34159  qqhcn  34362  esumpr2  34438  esumpfinval  34446  esumpfinvalf  34447  carsggect  34689  oddpwdcv  34726  eulerpartlemgs2  34751  fibp1  34772  orvcelval  34840  ballotlemscr  34890  ballotlemfrci  34899  signsplypnf  34918  reprpmtf1o  34994  breprexplemc  35000  breprexp  35001  circlemeth  35008  lpadright  35055  revwlk  35598  subfacp1lem5  35657  cvmliftlem10  35767  circum  36147  faclimlem3  36218  fwddifnp1  36638  bj-bary1lem  37935  qdiff  37952  tan2h  38244  poimirlem3  38255  poimirlem13  38265  poimirlem14  38266  itgaddnclem1  38310  itgmulc2nclem2  38319  areacirclem1  38340  areacirclem4  38343  istotbnd3  38403  iscringd  38630  3atlem1  40238  pmod2iN  40604  polval2N  40661  lhple  40797  cdleme2  40983  cdleme35d  41207  cdleme42h  41237  cdlemeg46ngfr  41273  cdlemkid1  41677  lcfl7lem  42254  mapdpglem22  42448  mapdh6dN  42494  hdmap1l6d  42568  hdmapinvlem3  42675  lcmineqlem3  42779  readvrec2  43103  readdsub  43126  sn-negex12  43159  zmulcomlem  43222  evlselv  43304  evlsmhpvvval  43310  prjspeclsp  43327  prjspner1  43341  3cubeslem3r  43401  diophin  43486  irrapxlem2  43533  pellexlem6  43544  pell1234qrmulcl  43565  rmxyval  43625  rmxyneg  43630  rmxyadd  43631  jm2.24  43673  jm2.25  43709  limexissupab  43993  omabs2  44042  tfsconcatrev  44058  naddwordnexlem4  44111  snhesn  44495  radcnvrat  45007  binomcxplemnotnn0  45049  sub2times  45975  mul13d  45982  fperiodmullem  46005  fperiodmul  46006  isumneg  46301  climneg  46309  itgsinexp  46652  stoweidlem13  46710  stoweidlem42  46739  wallispilem4  46765  wallispilem5  46766  wallispi2lem1  46768  stirlinglem1  46771  stirlinglem3  46773  stirlinglem4  46774  stirlinglem5  46775  stirlinglem7  46777  stirlinglem10  46780  dirkertrigeqlem3  46797  fourierdlem30  46834  fourierdlem32  46836  fourierdlem42  46846  fourierdlem48  46851  fourierdlem49  46852  fourierdlem83  46886  sqwvfoura  46925  sqwvfourb  46926  etransclem2  46933  etransclem46  46977  sharhght  47562  sin3t  47591  sin5tlem1  47593  sin5tlem3  47595  cos5t  47599  imasetpreimafvbijlemfv  48134  fmtnorec3  48283  quad1  48368  requad1  48370  ushggricedg  48675  lmodvsmdi  49142  dmatALTbas  49164  ldepsprlem  49235  itcovalt2lem2lem2  49437  ackval3  49446  1subrec1sub  49468  eenglngeehlnmlem1  49500  eenglngeehlnmlem2  49501  itsclc0xyqsolr  49532  swapfid  50040  sinhpcosh  50501