Theorem 3eqtr2d 2770

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

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

This theorem is referenced by:  fmptapd  7145  negsub  11470  neg2sub  11482  divmuleq  11887  divneg2  11906  discr  14205  bcpasc  14286  hashgval2  14343  hashf1lem2  14421  relexpaddnn  15017  crim  15081  remullem  15094  isum1p  15807  geo2sum  15839  fallfacfwd  16002  fsumkthpow  16022  bpoly3  16024  bpoly4  16025  efi4p  16105  sinhval  16122  addcos  16142  cos2tsin  16147  demoivreALT  16169  rpnnen2lem11  16192  omeo  16336  pwp1fsum  16361  sadaddlem  16436  bitsres  16443  smumullem  16462  sqgcd  16532  expgcd  16533  eulerthlem2  16752  vfermltlALT  16773  pockthlem  16876  4sqlem10  16918  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  fuccocl  17929  resssetc  18054  resscatc  18071  uncfcurf  18200  yonedalem3b  18240  prdspjmhm  18756  grpinvid2  18924  imasgrp2  18987  mulgaddcomlem  19029  mulgmodid  19045  lagsubg2  19126  cntzsgrpcl  19266  cntzsubm  19270  sylow3lem2  19558  efgredleme  19673  ablsubsub  19747  ablsubsub4  19748  odadd2  19779  gex2abl  19781  pgpfac1lem3a  20008  pwspjmhmmgpd  20237  rngcid  20544  ringcid  20573  abvneg  20735  lmodfopne  20806  lsppr  21000  rngqiprngfulem4  21224  gzrngunit  21350  frlmsubgval  21674  frlmgsum  21681  psrass1  21873  resspsradd  21884  resspsrvsca  21886  mplcoe5  21947  mplmon2mul  21976  evlslem2  21986  evlsvarsrng  22006  coe1tm  22159  ply1scl1OLD  22180  ply1fermltlchr  22199  evls1varsrng  22227  mamuass  22289  mavmulass  22436  mulmarep1gsum2  22461  mdetuni0  22508  maducoeval2  22527  madulid  22532  mat2pmatmul  22618  decpmatmulsumfsupp  22660  pmatcollpwlem  22667  pm2mpmhmlem1  22705  cmpfi  23295  cnconn  23309  txrest  23518  utopsnneiplem  24135  blcvx  24686  tcphcphlem2  25136  cphipval2  25141  cphipval  25143  rrx0  25297  minveclem2  25326  pjthlem1  25337  uniioovol  25480  uniioombllem2  25484  itg1addlem4  25600  mbfi1fseqlem5  25620  itg2mulc  25648  itg2monolem1  25651  itgaddlem1  25724  itgmulc2lem2  25734  dvrec  25859  lhop2  25920  ftc1lem5  25947  deg1submon1p  26058  plypf1  26117  coefv0  26153  coemulhi  26159  coemulc  26160  dgreq0  26171  dvply1  26191  vieta1  26220  aareccl  26234  aaliou3lem8  26253  dvtaylp  26278  mtest  26313  sineq0  26433  efif1olem2  26452  efif1olem4  26454  tanarg  26528  logtayl2  26571  nnlogbexp  26691  isosctrlem2  26729  chordthmlem2  26743  chordthmlem4  26745  heron  26748  dcubic1lem  26753  dcubic1  26755  mcubic  26757  dquart  26763  quart1lem  26765  quart1  26766  efiasin  26798  asinsin  26802  atancj  26820  efiatan  26822  atanlogaddlem  26823  cosatan  26831  atantan  26833  atans2  26841  log2cnv  26854  log2tlbnd  26855  birthdaylem2  26862  cxplim  26882  lgamgulmlem2  26940  wilthlem1  26978  basellem3  26993  musum  27101  musumsum  27102  muinv  27103  pclogsum  27126  mersenne  27138  dchrabs  27171  dchrinv  27172  lgseisenlem1  27286  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  lgsquad2lem1  27295  2lgslem1  27305  2sqmod  27347  chebbnd1lem3  27382  chpchtlim  27390  rplogsumlem2  27396  dchrisumlem2  27401  dchrmusum2  27405  mulog2sumlem1  27445  mulog2sumlem3  27447  vmalogdivsum2  27449  selberg4lem1  27471  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntibndlem2  27502  pntlemr  27513  pntlemf  27516  pntlemo  27518  addsdilem4  28057  mulsunif2lem  28072  halfcut  28333  zs12bday  28343  ragcom  28625  colperpexlem1  28657  lmiisolem  28723  hypcgrlem2  28727  trgcopyeulem  28732  brbtwn2  28832  colinearalglem1  28833  colinearalglem2  28834  axcontlem2  28892  axcontlem8  28898  numedglnl  29071  clwlkclwwlklem2a  29927  numclwlk1lem1  30298  numclwlk1lem2  30299  numclwwlk2  30310  grpoinvid2  30458  ablodivdiv4  30483  smcnlem  30626  ipidsq  30639  ipasslem2  30761  minvecolem2  30804  hv2times  30990  pjhthlem1  31320  pjds3i  31642  ho2times  31748  opsqrlem6  32074  pjclem4  32128  pj3si  32136  csmdsymi  32263  ofoprabco  32588  fcnvgreu  32597  quad3d  32673  swrdrndisj  32879  trsp2cyc  33080  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  conjga  33127  elrgspnlem1  33193  rlocmulval  33220  imaslmod  33324  1arithufdlem3  33517  r1padd1  33573  frlmdim  33607  rrxdim  33610  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  extdg1id  33661  ccfldextdgrr  33667  fldextrspunlem1  33670  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  constrrecl  33759  constrresqrtcl  33767  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminply  33778  qqhcn  33981  esumpr2  34057  esumpfinval  34065  esumpfinvalf  34066  carsggect  34309  oddpwdcv  34346  eulerpartlemgs2  34371  fibp1  34392  orvcelval  34460  ballotlemscr  34510  ballotlemfrci  34519  signsplypnf  34541  reprpmtf1o  34617  breprexplemc  34623  breprexp  34624  circlemeth  34631  lpadright  34675  revwlk  35112  subfacp1lem5  35171  cvmliftlem10  35281  circum  35661  faclimlem3  35732  fwddifnp1  36153  bj-bary1lem  37298  tan2h  37606  poimirlem3  37617  poimirlem13  37627  poimirlem14  37628  itgaddnclem1  37672  itgmulc2nclem2  37681  areacirclem1  37702  areacirclem4  37705  istotbnd3  37765  iscringd  37992  3atlem1  39477  pmod2iN  39843  polval2N  39900  lhple  40036  cdleme2  40222  cdleme35d  40446  cdleme42h  40476  cdlemeg46ngfr  40512  cdlemkid1  40916  lcfl7lem  41493  mapdpglem22  41687  mapdh6dN  41733  hdmap1l6d  41807  hdmapinvlem3  41914  lcmineqlem3  42019  nnadddir  42258  readvrec2  42349  readdsub  42372  sn-negex12  42405  zmulcomlem  42455  selvvvval  42573  evlselv  42575  evlsmhpvvval  42583  prjspeclsp  42600  prjspner1  42614  3cubeslem3r  42675  diophin  42760  irrapxlem2  42811  pellexlem6  42822  pell1234qrmulcl  42843  rmxyval  42904  rmxyneg  42909  rmxyadd  42910  jm2.24  42952  jm2.25  42988  limexissupab  43272  omabs2  43321  tfsconcatrev  43337  naddwordnexlem4  43390  snhesn  43775  scottrankd  44237  radcnvrat  44303  binomcxplemnotnn0  44345  sub2times  45271  mul13d  45278  fperiodmullem  45301  fperiodmul  45302  isumneg  45600  climneg  45608  itgsinexp  45953  stoweidlem13  46011  stoweidlem42  46040  wallispilem4  46066  wallispilem5  46067  wallispi2lem1  46069  stirlinglem1  46072  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem7  46078  stirlinglem10  46081  dirkertrigeqlem3  46098  fourierdlem30  46135  fourierdlem32  46137  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem83  46187  sqwvfoura  46226  sqwvfourb  46227  etransclem2  46234  etransclem46  46278  sharhght  46863  imasetpreimafvbijlemfv  47403  fmtnorec3  47549  quad1  47621  requad1  47623  ushggricedg  47927  lmodvsmdi  48367  dmatALTbas  48390  ldepsprlem  48461  itcovalt2lem2lem2  48663  ackval3  48672  1subrec1sub  48694  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  itsclc0xyqsolr  48758  swapfid  49268  sinhpcosh  49729