Theorem 3eqtr2d 2662

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 2659	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtrd 2656	1 |- ( ph -> A = D )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  fmptapd  6437  negsub  10329  neg2sub  10341  divmuleq  10730  divneg2  10749  discr  13001  bcpasc  13108  hashgval2  13167  hashf1lem2  13240  relexpaddnn  13791  crim  13855  remullem  13868  isum1p  14573  geo2sum  14604  fallfacfwd  14767  fsumkthpow  14787  bpoly3  14789  bpoly4  14790  efi4p  14867  sinhval  14884  addcos  14904  cos2tsin  14909  demoivreALT  14931  rpnnen2lem11  14953  omeo  15090  pwp1fsum  15114  sadaddlem  15188  bitsres  15195  smumullem  15214  sqgcd  15278  eulerthlem2  15487  vfermltlALT  15507  pockthlem  15609  4sqlem10  15651  vdwlem2  15686  vdwlem6  15690  vdwlem8  15692  fuccocl  16624  resssetc  16742  resscatc  16755  uncfcurf  16879  yonedalem3b  16919  prdspjmhm  17367  grpinvid2  17471  imasgrp2  17530  mulgaddcomlem  17563  mulgmodid  17581  lagsubg2  17655  cntzsubm  17768  sylow3lem2  18043  efgredleme  18156  ablsubsub  18223  ablsubsub4  18224  odadd2  18252  gex2abl  18254  pgpfac1lem3a  18475  abvneg  18834  lmodfopne  18901  lsppr  19093  psrass1  19405  resspsradd  19416  resspsrvsca  19418  mplcoe5  19468  mplmon2mul  19501  evlslem2  19512  evlsvarsrng  19528  coe1tm  19643  ply1scl1  19662  evls1varsrng  19704  gzrngunit  19812  frlmsubgval  20108  frlmgsum  20111  mamuass  20208  mavmulass  20355  mulmarep1gsum2  20380  mdetuni0  20427  maducoeval2  20446  madulid  20451  mat2pmatmul  20536  decpmatmulsumfsupp  20578  pmatcollpwlem  20585  pm2mpmhmlem1  20623  cmpfi  21211  cnconn  21225  txrest  21434  utopsnneiplem  22051  blcvx  22601  tchcphlem2  23035  cphipval2  23040  cphipval  23042  minveclem2  23197  pjthlem1  23208  uniioovol  23347  uniioombllem2  23351  itg1addlem4  23466  mbfi1fseqlem5  23486  itg2mulc  23514  itg2monolem1  23517  itgaddlem1  23589  itgmulc2lem2  23599  dvrec  23718  lhop2  23778  ftc1lem5  23803  deg1submon1p  23912  plypf1  23968  coefv0  24004  coemulhi  24010  coemulc  24011  dgreq0  24021  dvply1  24039  vieta1  24067  aareccl  24081  aaliou3lem8  24100  dvtaylp  24124  mtest  24158  sineq0  24273  efif1olem2  24289  efif1olem4  24291  tanarg  24365  logtayl2  24408  nnlogbexp  24519  isosctrlem2  24549  chordthmlem2  24560  chordthmlem4  24562  heron  24565  dcubic1lem  24570  dcubic1  24572  mcubic  24574  dquart  24580  quart1lem  24582  quart1  24583  efiasin  24615  asinsin  24619  atancj  24637  efiatan  24639  atanlogaddlem  24640  cosatan  24648  atantan  24650  atans2  24658  log2cnv  24671  log2tlbnd  24672  birthdaylem2  24679  cxplim  24698  lgamgulmlem2  24756  wilthlem1  24794  basellem3  24809  musum  24917  musumsum  24918  muinv  24919  pclogsum  24940  mersenne  24952  dchrabs  24985  dchrinv  24986  lgseisenlem1  25100  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem1  25109  2lgslem1  25119  chebbnd1lem3  25160  chpchtlim  25168  rplogsumlem2  25174  dchrisumlem2  25179  dchrmusum2  25183  mulog2sumlem1  25223  mulog2sumlem3  25225  vmalogdivsum2  25227  selberg4lem1  25249  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  pntibndlem2  25280  pntlemr  25291  pntlemf  25294  pntlemo  25296  ragcom  25593  colperpexlem1  25622  lmiisolem  25688  hypcgrlem2  25692  trgcopyeulem  25697  brbtwn2  25785  colinearalglem1  25786  colinearalglem2  25787  axcontlem2  25845  axcontlem8  25851  basvtxvalOLD  25903  numedglnl  26039  clwlkclwwlklem2a  26899  numclwwlk2  27240  grpoinvid2  27383  ablodivdiv4  27408  smcnlem  27552  ipidsq  27565  ipasslem2  27687  minvecolem2  27731  hv2times  27918  pjhthlem1  28250  pjds3i  28572  ho2times  28678  opsqrlem6  29004  pjclem4  29058  pj3si  29066  csmdsymi  29193  ofoprabco  29464  fcnvgreu  29472  2sqmod  29648  qqhcn  30035  esumpr2  30129  esumpfinval  30137  esumpfinvalf  30138  carsggect  30380  oddpwdcv  30417  eulerpartlemgs2  30442  fibp1  30463  orvcelval  30530  ballotlemscr  30580  ballotlemfrci  30589  signsplypnf  30627  reprpmtf1o  30704  breprexplemc  30710  breprexp  30711  circlemeth  30718  subfacp1lem5  31166  cvmliftlem10  31276  circum  31568  faclimlem3  31631  fwddifnp1  32272  bj-bary1lem  33160  tan2h  33401  poimirlem3  33412  poimirlem13  33422  poimirlem14  33423  itgaddnclem1  33468  itgmulc2nclem2  33477  areacirclem1  33500  areacirclem4  33503  istotbnd3  33570  iscringd  33797  3atlem1  34769  pmod2iN  35135  polval2N  35192  lhple  35328  cdleme2  35515  cdleme35d  35740  cdleme42h  35770  cdlemeg46ngfr  35806  cdlemkid1  36210  lcfl7lem  36788  mapdpglem22  36982  mapdh6dN  37028  hdmap1l6d  37103  hdmapinvlem3  37212  diophin  37336  irrapxlem2  37387  pellexlem6  37398  pell1234qrmulcl  37419  rmxyval  37480  rmxyneg  37485  rmxyadd  37486  jm2.24  37530  jm2.25  37566  snhesn  38080  radcnvrat  38513  binomcxplemnotnn0  38555  sub2times  39485  mul13d  39491  fperiodmullem  39517  fperiodmul  39518  isumneg  39834  climneg  39842  itgsinexp  40170  stoweidlem13  40230  stoweidlem42  40259  wallispilem4  40285  wallispilem5  40286  wallispi2lem1  40288  stirlinglem1  40291  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem7  40297  stirlinglem10  40300  dirkertrigeqlem3  40317  fourierdlem30  40354  fourierdlem32  40356  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem83  40406  sqwvfoura  40445  sqwvfourb  40446  etransclem2  40453  etransclem46  40497  sharhght  41054  fmtnorec3  41460  rngcid  41979  ringcid  42025  lmodvsmdi  42163  dmatALTbas  42190  ldepsprlem  42261  sinhpcosh  42481