Theorem 3eqtr2d 2771

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  fmptapd  7148  negsub  11477  neg2sub  11489  divmuleq  11894  divneg2  11913  discr  14212  bcpasc  14293  hashgval2  14350  hashf1lem2  14428  relexpaddnn  15024  crim  15088  remullem  15101  isum1p  15814  geo2sum  15846  fallfacfwd  16009  fsumkthpow  16029  bpoly3  16031  bpoly4  16032  efi4p  16112  sinhval  16129  addcos  16149  cos2tsin  16154  demoivreALT  16176  rpnnen2lem11  16199  omeo  16343  pwp1fsum  16368  sadaddlem  16443  bitsres  16450  smumullem  16469  sqgcd  16539  expgcd  16540  eulerthlem2  16759  vfermltlALT  16780  pockthlem  16883  4sqlem10  16925  vdwlem2  16960  vdwlem6  16964  vdwlem8  16966  fuccocl  17936  resssetc  18061  resscatc  18078  uncfcurf  18207  yonedalem3b  18247  prdspjmhm  18763  grpinvid2  18931  imasgrp2  18994  mulgaddcomlem  19036  mulgmodid  19052  lagsubg2  19133  cntzsgrpcl  19273  cntzsubm  19277  sylow3lem2  19565  efgredleme  19680  ablsubsub  19754  ablsubsub4  19755  odadd2  19786  gex2abl  19788  pgpfac1lem3a  20015  pwspjmhmmgpd  20244  rngcid  20551  ringcid  20580  abvneg  20742  lmodfopne  20813  lsppr  21007  rngqiprngfulem4  21231  gzrngunit  21357  frlmsubgval  21681  frlmgsum  21688  psrass1  21880  resspsradd  21891  resspsrvsca  21893  mplcoe5  21954  mplmon2mul  21983  evlslem2  21993  evlsvarsrng  22013  coe1tm  22166  ply1scl1OLD  22187  ply1fermltlchr  22206  evls1varsrng  22234  mamuass  22296  mavmulass  22443  mulmarep1gsum2  22468  mdetuni0  22515  maducoeval2  22534  madulid  22539  mat2pmatmul  22625  decpmatmulsumfsupp  22667  pmatcollpwlem  22674  pm2mpmhmlem1  22712  cmpfi  23302  cnconn  23316  txrest  23525  utopsnneiplem  24142  blcvx  24693  tcphcphlem2  25143  cphipval2  25148  cphipval  25150  rrx0  25304  minveclem2  25333  pjthlem1  25344  uniioovol  25487  uniioombllem2  25491  itg1addlem4  25607  mbfi1fseqlem5  25627  itg2mulc  25655  itg2monolem1  25658  itgaddlem1  25731  itgmulc2lem2  25741  dvrec  25866  lhop2  25927  ftc1lem5  25954  deg1submon1p  26065  plypf1  26124  coefv0  26160  coemulhi  26166  coemulc  26167  dgreq0  26178  dvply1  26198  vieta1  26227  aareccl  26241  aaliou3lem8  26260  dvtaylp  26285  mtest  26320  sineq0  26440  efif1olem2  26459  efif1olem4  26461  tanarg  26535  logtayl2  26578  nnlogbexp  26698  isosctrlem2  26736  chordthmlem2  26750  chordthmlem4  26752  heron  26755  dcubic1lem  26760  dcubic1  26762  mcubic  26764  dquart  26770  quart1lem  26772  quart1  26773  efiasin  26805  asinsin  26809  atancj  26827  efiatan  26829  atanlogaddlem  26830  cosatan  26838  atantan  26840  atans2  26848  log2cnv  26861  log2tlbnd  26862  birthdaylem2  26869  cxplim  26889  lgamgulmlem2  26947  wilthlem1  26985  basellem3  27000  musum  27108  musumsum  27109  muinv  27110  pclogsum  27133  mersenne  27145  dchrabs  27178  dchrinv  27179  lgseisenlem1  27293  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  lgsquad2lem1  27302  2lgslem1  27312  2sqmod  27354  chebbnd1lem3  27389  chpchtlim  27397  rplogsumlem2  27403  dchrisumlem2  27408  dchrmusum2  27412  mulog2sumlem1  27452  mulog2sumlem3  27454  vmalogdivsum2  27456  selberg4lem1  27478  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntibndlem2  27509  pntlemr  27520  pntlemf  27523  pntlemo  27525  addsdilem4  28064  mulsunif2lem  28079  halfcut  28340  zs12bday  28350  ragcom  28632  colperpexlem1  28664  lmiisolem  28730  hypcgrlem2  28734  trgcopyeulem  28739  brbtwn2  28839  colinearalglem1  28840  colinearalglem2  28841  axcontlem2  28899  axcontlem8  28905  numedglnl  29078  clwlkclwwlklem2a  29934  numclwlk1lem1  30305  numclwlk1lem2  30306  numclwwlk2  30317  grpoinvid2  30465  ablodivdiv4  30490  smcnlem  30633  ipidsq  30646  ipasslem2  30768  minvecolem2  30811  hv2times  30997  pjhthlem1  31327  pjds3i  31649  ho2times  31755  opsqrlem6  32081  pjclem4  32135  pj3si  32143  csmdsymi  32270  ofoprabco  32595  fcnvgreu  32604  quad3d  32680  swrdrndisj  32886  trsp2cyc  33087  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2  33097  conjga  33134  elrgspnlem1  33200  rlocmulval  33227  imaslmod  33331  1arithufdlem3  33524  r1padd1  33580  frlmdim  33614  rrxdim  33617  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  extdg1id  33668  ccfldextdgrr  33674  fldextrspunlem1  33677  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  constrrecl  33766  constrresqrtcl  33774  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminply  33785  qqhcn  33988  esumpr2  34064  esumpfinval  34072  esumpfinvalf  34073  carsggect  34316  oddpwdcv  34353  eulerpartlemgs2  34378  fibp1  34399  orvcelval  34467  ballotlemscr  34517  ballotlemfrci  34526  signsplypnf  34548  reprpmtf1o  34624  breprexplemc  34630  breprexp  34631  circlemeth  34638  lpadright  34682  revwlk  35119  subfacp1lem5  35178  cvmliftlem10  35288  circum  35668  faclimlem3  35739  fwddifnp1  36160  bj-bary1lem  37305  tan2h  37613  poimirlem3  37624  poimirlem13  37634  poimirlem14  37635  itgaddnclem1  37679  itgmulc2nclem2  37688  areacirclem1  37709  areacirclem4  37712  istotbnd3  37772  iscringd  37999  3atlem1  39484  pmod2iN  39850  polval2N  39907  lhple  40043  cdleme2  40229  cdleme35d  40453  cdleme42h  40483  cdlemeg46ngfr  40519  cdlemkid1  40923  lcfl7lem  41500  mapdpglem22  41694  mapdh6dN  41740  hdmap1l6d  41814  hdmapinvlem3  41921  lcmineqlem3  42026  nnadddir  42265  readvrec2  42356  readdsub  42379  sn-negex12  42412  zmulcomlem  42462  selvvvval  42580  evlselv  42582  evlsmhpvvval  42590  prjspeclsp  42607  prjspner1  42621  3cubeslem3r  42682  diophin  42767  irrapxlem2  42818  pellexlem6  42829  pell1234qrmulcl  42850  rmxyval  42911  rmxyneg  42916  rmxyadd  42917  jm2.24  42959  jm2.25  42995  limexissupab  43279  omabs2  43328  tfsconcatrev  43344  naddwordnexlem4  43397  snhesn  43782  scottrankd  44244  radcnvrat  44310  binomcxplemnotnn0  44352  sub2times  45278  mul13d  45285  fperiodmullem  45308  fperiodmul  45309  isumneg  45607  climneg  45615  itgsinexp  45960  stoweidlem13  46018  stoweidlem42  46047  wallispilem4  46073  wallispilem5  46074  wallispi2lem1  46076  stirlinglem1  46079  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem7  46085  stirlinglem10  46088  dirkertrigeqlem3  46105  fourierdlem30  46142  fourierdlem32  46144  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem83  46194  sqwvfoura  46233  sqwvfourb  46234  etransclem2  46241  etransclem46  46285  sharhght  46870  imasetpreimafvbijlemfv  47407  fmtnorec3  47553  quad1  47625  requad1  47627  ushggricedg  47931  lmodvsmdi  48371  dmatALTbas  48394  ldepsprlem  48465  itcovalt2lem2lem2  48667  ackval3  48676  1subrec1sub  48698  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  itsclc0xyqsolr  48762  swapfid  49272  sinhpcosh  49733