Theorem 3eqtr2d 2777

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

Syntax hints:   → wi 4   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  fmptapd  6964  negsub  11091  neg2sub  11103  divmuleq  11502  divneg2  11521  discr  13772  bcpasc  13852  hashgval2  13910  hashf1lem2  13987  relexpaddnn  14579  crim  14643  remullem  14656  isum1p  15368  geo2sum  15400  fallfacfwd  15561  fsumkthpow  15581  bpoly3  15583  bpoly4  15584  efi4p  15661  sinhval  15678  addcos  15698  cos2tsin  15703  demoivreALT  15725  rpnnen2lem11  15748  omeo  15890  pwp1fsum  15915  sadaddlem  15988  bitsres  15995  smumullem  16014  sqgcd  16085  eulerthlem2  16298  vfermltlALT  16318  pockthlem  16421  4sqlem10  16463  vdwlem2  16498  vdwlem6  16502  vdwlem8  16504  fuccocl  17427  resssetc  17552  resscatc  17569  uncfcurf  17701  yonedalem3b  17741  prdspjmhm  18209  grpinvid2  18373  imasgrp2  18432  mulgaddcomlem  18468  mulgmodid  18484  lagsubg2  18559  cntzsubm  18684  sylow3lem2  18971  efgredleme  19087  ablsubsub  19157  ablsubsub4  19158  odadd2  19188  gex2abl  19190  pgpfac1lem3a  19417  abvneg  19824  lmodfopne  19891  lsppr  20084  gzrngunit  20383  frlmsubgval  20681  frlmgsum  20688  psrass1  20884  resspsradd  20895  resspsrvsca  20897  mplcoe5  20951  mplmon2mul  20981  evlslem2  20993  evlsvarsrng  21013  coe1tm  21148  ply1scl1  21167  evls1varsrng  21210  mamuass  21253  mavmulass  21400  mulmarep1gsum2  21425  mdetuni0  21472  maducoeval2  21491  madulid  21496  mat2pmatmul  21582  decpmatmulsumfsupp  21624  pmatcollpwlem  21631  pm2mpmhmlem1  21669  cmpfi  22259  cnconn  22273  txrest  22482  utopsnneiplem  23099  blcvx  23649  tcphcphlem2  24087  cphipval2  24092  cphipval  24094  rrx0  24248  minveclem2  24277  pjthlem1  24288  uniioovol  24430  uniioombllem2  24434  itg1addlem4  24550  itg1addlem4OLD  24551  mbfi1fseqlem5  24571  itg2mulc  24599  itg2monolem1  24602  itgaddlem1  24674  itgmulc2lem2  24684  dvrec  24806  lhop2  24866  ftc1lem5  24891  deg1submon1p  25004  plypf1  25060  coefv0  25096  coemulhi  25102  coemulc  25103  dgreq0  25113  dvply1  25131  vieta1  25159  aareccl  25173  aaliou3lem8  25192  dvtaylp  25216  mtest  25250  sineq0  25367  efif1olem2  25386  efif1olem4  25388  tanarg  25461  logtayl2  25504  nnlogbexp  25618  isosctrlem2  25656  chordthmlem2  25670  chordthmlem4  25672  heron  25675  dcubic1lem  25680  dcubic1  25682  mcubic  25684  dquart  25690  quart1lem  25692  quart1  25693  efiasin  25725  asinsin  25729  atancj  25747  efiatan  25749  atanlogaddlem  25750  cosatan  25758  atantan  25760  atans2  25768  log2cnv  25781  log2tlbnd  25782  birthdaylem2  25789  cxplim  25808  lgamgulmlem2  25866  wilthlem1  25904  basellem3  25919  musum  26027  musumsum  26028  muinv  26029  pclogsum  26050  mersenne  26062  dchrabs  26095  dchrinv  26096  lgseisenlem1  26210  lgsquadlem1  26215  lgsquadlem2  26216  lgsquadlem3  26217  lgsquad2lem1  26219  2lgslem1  26229  2sqmod  26271  chebbnd1lem3  26306  chpchtlim  26314  rplogsumlem2  26320  dchrisumlem2  26325  dchrmusum2  26329  mulog2sumlem1  26369  mulog2sumlem3  26371  vmalogdivsum2  26373  selberg4lem1  26395  pntrlog2bndlem2  26413  pntrlog2bndlem4  26415  pntibndlem2  26426  pntlemr  26437  pntlemf  26440  pntlemo  26442  ragcom  26743  colperpexlem1  26775  lmiisolem  26841  hypcgrlem2  26845  trgcopyeulem  26850  brbtwn2  26950  colinearalglem1  26951  colinearalglem2  26952  axcontlem2  27010  axcontlem8  27016  numedglnl  27189  clwlkclwwlklem2a  28035  numclwlk1lem1  28406  numclwlk1lem2  28407  numclwwlk2  28418  grpoinvid2  28564  ablodivdiv4  28589  smcnlem  28732  ipidsq  28745  ipasslem2  28867  minvecolem2  28910  hv2times  29096  pjhthlem1  29426  pjds3i  29748  ho2times  29854  opsqrlem6  30180  pjclem4  30234  pj3si  30242  csmdsymi  30369  ofoprabco  30675  fcnvgreu  30684  swrdrndisj  30903  trsp2cyc  31063  cycpmco2lem3  31068  cycpmco2lem4  31069  cycpmco2lem5  31070  cycpmco2lem6  31071  cycpmco2  31073  imaslmod  31221  ply1fermltl  31338  frlmdim  31362  rrxdim  31365  lbsdiflsp0  31375  fedgmullem1  31378  fedgmullem2  31379  extdg1id  31406  ccfldextdgrr  31410  qqhcn  31607  esumpr2  31701  esumpfinval  31709  esumpfinvalf  31710  carsggect  31951  oddpwdcv  31988  eulerpartlemgs2  32013  fibp1  32034  orvcelval  32101  ballotlemscr  32151  ballotlemfrci  32160  signsplypnf  32195  reprpmtf1o  32272  breprexplemc  32278  breprexp  32279  circlemeth  32286  lpadright  32330  revwlk  32753  subfacp1lem5  32813  cvmliftlem10  32923  circum  33299  faclimlem3  33380  fwddifnp1  34153  bj-bary1lem  35164  tan2h  35455  poimirlem3  35466  poimirlem13  35476  poimirlem14  35477  itgaddnclem1  35521  itgmulc2nclem2  35530  areacirclem1  35551  areacirclem4  35554  istotbnd3  35615  iscringd  35842  3atlem1  37183  pmod2iN  37549  polval2N  37606  lhple  37742  cdleme2  37928  cdleme35d  38152  cdleme42h  38182  cdlemeg46ngfr  38218  cdlemkid1  38622  lcfl7lem  39199  mapdpglem22  39393  mapdh6dN  39439  hdmap1l6d  39513  hdmapinvlem3  39620  lcmineqlem3  39722  pwspjmhmmgpd  39920  nnadddir  39948  expgcd  39983  readdsub  40016  sn-negex12  40047  prjspeclsp  40100  prjspner1  40112  3cubeslem3r  40153  diophin  40238  irrapxlem2  40289  pellexlem6  40300  pell1234qrmulcl  40321  rmxyval  40381  rmxyneg  40386  rmxyadd  40387  jm2.24  40429  jm2.25  40465  snhesn  41012  scottrankd  41480  radcnvrat  41546  binomcxplemnotnn0  41588  sub2times  42426  mul13d  42431  fperiodmullem  42456  fperiodmul  42457  isumneg  42761  climneg  42769  itgsinexp  43114  stoweidlem13  43172  stoweidlem42  43201  wallispilem4  43227  wallispilem5  43228  wallispi2lem1  43230  stirlinglem1  43233  stirlinglem3  43235  stirlinglem4  43236  stirlinglem5  43237  stirlinglem7  43239  stirlinglem10  43242  dirkertrigeqlem3  43259  fourierdlem30  43296  fourierdlem32  43298  fourierdlem42  43308  fourierdlem48  43313  fourierdlem49  43314  fourierdlem83  43348  sqwvfoura  43387  sqwvfourb  43388  etransclem2  43395  etransclem46  43439  sharhght  43996  imasetpreimafvbijlemfv  44470  fmtnorec3  44616  quad1  44688  requad1  44690  isomgreqve  44893  ushrisomgr  44909  rngcid  45153  ringcid  45199  lmodvsmdi  45334  dmatALTbas  45358  ldepsprlem  45429  itcovalt2lem2lem2  45636  ackval3  45645  1subrec1sub  45667  eenglngeehlnmlem1  45699  eenglngeehlnmlem2  45700  itsclc0xyqsolr  45731  sinhpcosh  46056