Theorem 3eqtr2d 2507

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

Hypotheses

Ref	Expression
3eqtr2d.1	|- ( ph -> A = B )
3eqtr2d.2	|- ( ph -> C = B )
3eqtr2d.3	|- ( ph -> C = D )

Assertion

Ref	Expression
3eqtr2d	|- ( ph -> A = D )

Proof of Theorem 3eqtr2d

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 |- ( ph -> A = B )
2		3eqtr2d.2	. . 3 |- ( ph -> C = B )
3	1, 2	eqtr4d 2504	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtrd 2501	1 |- ( ph -> A = D )

Syntax hints:   -> wi 4   = wceq 1374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-cleq 2452

This theorem is referenced by:  fmptapd  6076  negsub  9856  neg2sub  9868  divmuleq  10238  divneg2  10257  discr  12258  bcpasc  12354  hashgval2  12401  hashf1lem2  12458  crim  12898  remullem  12911  incexclem  13600  isum1p  13605  geo2sum  13634  efi4p  13722  sinhval  13739  addcos  13759  cos2tsin  13764  demoivreALT  13786  rpnnen2lem11  13808  sadaddlem  13964  smumullem  13990  sqgcd  14044  eulerthlem2  14160  omeo  14186  pockthlem  14271  4sqlem10  14313  vdwlem2  14348  vdwlem6  14352  vdwlem8  14354  fuccocl  15180  resssetc  15266  resscatc  15279  uncfcurf  15355  yonedalem3b  15395  prdspjmhm  15801  grpinvid2  15893  imasgrp2  15978  lagsubg2  16050  cntzsubm  16161  sylow3lem2  16437  efgredleme  16550  ablsubsub  16617  ablsubsub4  16618  odadd2  16641  gex2abl  16643  pgpfac1lem3a  16910  abvneg  17259  lsppr  17515  psrass1  17824  resspsradd  17835  resspsrvsca  17837  mplcoe5  17895  mplcoe2OLD  17897  mplmon2mul  17930  evlslem2  17944  evlsvarsrng  17961  coe1tm  18078  ply1scl1  18097  evls1varsrng  18140  gzrngunit  18244  frlmsubgval  18558  frlmgsumOLD  18561  frlmgsum  18562  mamuass  18664  mavmulass  18811  mulmarep1gsum2  18836  mdetuni0  18883  maducoeval2  18902  madulid  18907  mat2pmatmul  18992  decpmatmulsumfsupp  19034  pmatcollpwlem  19041  pm2mpmhmlem1  19079  cmpfi  19667  cnconn  19682  txrest  19860  utopsnneiplem  20478  blcvx  21031  tchcphlem2  21407  minveclem2  21569  pjthlem1  21580  uniioovol  21716  uniioombllem2  21720  itg1addlem4  21834  mbfi1fseqlem5  21854  itg2mulc  21882  itg2monolem1  21885  itgaddlem1  21957  itgmulc2lem2  21967  dvrec  22086  lhop2  22144  ftc1lem5  22169  deg1submon1p  22281  plypf1  22337  coefv0  22372  coemulhi  22378  coemulc  22379  dgreq0  22389  dvply1  22407  vieta1  22435  aareccl  22449  aaliou3lem8  22468  dvtaylp  22492  mtest  22526  sineq0  22640  efif1olem2  22656  efif1olem4  22658  tanarg  22725  logtayl2  22764  isosctrlem2  22874  chordthmlem2  22885  chordthmlem4  22887  heron  22890  dcubic1lem  22895  dcubic1  22897  mcubic  22899  dquart  22905  quart1lem  22907  quart1  22908  efiasin  22940  asinsin  22944  atancj  22962  efiatan  22964  atanlogaddlem  22965  cosatan  22973  atantan  22975  atans2  22983  log2cnv  22996  log2tlbnd  22997  birthdaylem2  23003  cxplim  23022  wilthlem1  23063  basellem3  23077  musum  23188  musumsum  23189  muinv  23190  pclogsum  23211  mersenne  23223  dchrabs  23256  dchrinv  23257  lgseisenlem1  23345  lgsquadlem1  23350  lgsquadlem2  23351  lgsquadlem3  23352  lgsquad2lem1  23354  chebbnd1lem3  23377  chpchtlim  23385  rplogsumlem2  23391  dchrisumlem2  23396  dchrmusum2  23400  mulog2sumlem1  23440  mulog2sumlem3  23442  vmalogdivsum2  23444  selberg4lem1  23466  pntrlog2bndlem2  23484  pntrlog2bndlem4  23486  pntibndlem2  23497  pntlemr  23508  pntlemf  23511  pntlemo  23513  ragcom  23776  colperpexlem1  23802  lmiisolem  23831  hypcgrlem2  23835  brbtwn2  23877  colinearalglem1  23878  colinearalglem2  23879  axcontlem2  23937  axcontlem8  23943  clwlkisclwwlklem2a  24447  grpoinvid2  24759  gxcom  24797  gxmodid  24807  ablodivdiv4  24819  vcoprne  24998  nvnncan  25084  smcnlem  25133  ipidsq  25149  ipasslem2  25273  minvecolem2  25317  hv2times  25504  pjhthlem1  25835  pjds3i  26157  ho2times  26264  opsqrlem6  26590  pjclem4  26644  pj3si  26652  csmdsymi  26779  ofoprabco  27027  fcnvgreu  27036  qqhcn  27458  nnlogbexp  27510  esumpr2  27564  esumpfinval  27571  esumpfinvalf  27572  oddpwdcv  27784  eulerpartlemgs2  27809  fibp1  27830  orvcelval  27897  ballotlemscr  27947  ballotlemfrci  27956  signsplypnf  27997  lgamgulmlem2  28062  subfacp1lem5  28118  cvmliftlem10  28229  fallfacfwd  28585  faclimlem3  28597  fsumkthpow  29245  bpoly3  29247  bpoly4  29248  tan2h  29475  mblfinlem2  29480  itgaddnclem1  29501  itgmulc2nclem2  29510  areacirclem1  29535  areacirclem4  29538  istotbnd3  29721  iscringd  29850  diophin  30161  irrapxlem2  30214  pellexlem6  30225  pell1234qrmulcl  30246  rmxyval  30306  rmxyadd  30312  jm2.24  30356  jm2.25  30398  isumneg  30963  climneg  30971  itgsinexp  31091  stoweidlem13  31132  stoweidlem42  31161  wallispilem4  31187  wallispilem5  31188  wallispi2lem1  31190  stirlinglem1  31193  stirlinglem3  31195  stirlinglem4  31196  stirlinglem5  31197  stirlinglem7  31199  stirlinglem10  31202  fourierdlem60  31286  sharhght  31368  numclwwlk2  31826  lmodvsmdi  31923  dmatALTbas  31950  ldepsprlem  32021  sinhpcosh  32090  bj-bary1lem  33626  3atlem1  34154  pmod2iN  34520  polval2N  34577  lhple  34713  cdleme2  34899  cdleme35d  35123  cdleme42h  35153  cdlemeg46ngfr  35189  cdlemkid1  35593  lcfl7lem  36171  mapdpglem22  36365  mapdh6dN  36411  hdmap1l6d  36486  hdmapinvlem3  36595