Theorem 3eqtr2d 2490

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

Syntax hints:   -> wi 4   = wceq 1383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

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

This theorem is referenced by:  fmptapd  6080  negsub  9872  neg2sub  9884  divmuleq  10255  divneg2  10274  discr  12282  bcpasc  12378  hashgval2  12425  hashf1lem2  12484  crim  12927  remullem  12940  incexclem  13627  isum1p  13632  geo2sum  13661  efi4p  13749  sinhval  13766  addcos  13786  cos2tsin  13791  demoivreALT  13813  rpnnen2lem11  13835  sadaddlem  13993  smumullem  14019  sqgcd  14073  eulerthlem2  14189  omeo  14215  pockthlem  14300  4sqlem10  14342  vdwlem2  14377  vdwlem6  14381  vdwlem8  14383  fuccocl  15207  resssetc  15293  resscatc  15306  uncfcurf  15382  yonedalem3b  15422  prdspjmhm  15872  grpinvid2  15973  imasgrp2  16059  lagsubg2  16136  cntzsubm  16247  sylow3lem2  16522  efgredleme  16635  ablsubsub  16702  ablsubsub4  16703  odadd2  16729  gex2abl  16731  pgpfac1lem3a  17001  abvneg  17357  lsppr  17613  psrass1  17934  resspsradd  17945  resspsrvsca  17947  mplcoe5  18005  mplcoe2OLD  18007  mplmon2mul  18040  evlslem2  18054  evlsvarsrng  18071  coe1tm  18188  ply1scl1  18207  evls1varsrng  18250  gzrngunit  18357  frlmsubgval  18671  frlmgsumOLD  18674  frlmgsum  18675  mamuass  18777  mavmulass  18924  mulmarep1gsum2  18949  mdetuni0  18996  maducoeval2  19015  madulid  19020  mat2pmatmul  19105  decpmatmulsumfsupp  19147  pmatcollpwlem  19154  pm2mpmhmlem1  19192  cmpfi  19781  cnconn  19796  txrest  20005  utopsnneiplem  20623  blcvx  21176  tchcphlem2  21552  minveclem2  21714  pjthlem1  21725  uniioovol  21861  uniioombllem2  21865  itg1addlem4  21979  mbfi1fseqlem5  21999  itg2mulc  22027  itg2monolem1  22030  itgaddlem1  22102  itgmulc2lem2  22112  dvrec  22231  lhop2  22289  ftc1lem5  22314  deg1submon1p  22426  plypf1  22482  coefv0  22517  coemulhi  22523  coemulc  22524  dgreq0  22534  dvply1  22552  vieta1  22580  aareccl  22594  aaliou3lem8  22613  dvtaylp  22637  mtest  22671  sineq0  22786  efif1olem2  22802  efif1olem4  22804  tanarg  22876  logtayl2  22915  isosctrlem2  23025  chordthmlem2  23036  chordthmlem4  23038  heron  23041  dcubic1lem  23046  dcubic1  23048  mcubic  23050  dquart  23056  quart1lem  23058  quart1  23059  efiasin  23091  asinsin  23095  atancj  23113  efiatan  23115  atanlogaddlem  23116  cosatan  23124  atantan  23126  atans2  23134  log2cnv  23147  log2tlbnd  23148  birthdaylem2  23154  cxplim  23173  wilthlem1  23214  basellem3  23228  musum  23339  musumsum  23340  muinv  23341  pclogsum  23362  mersenne  23374  dchrabs  23407  dchrinv  23408  lgseisenlem1  23496  lgsquadlem1  23501  lgsquadlem2  23502  lgsquadlem3  23503  lgsquad2lem1  23505  chebbnd1lem3  23528  chpchtlim  23536  rplogsumlem2  23542  dchrisumlem2  23547  dchrmusum2  23551  mulog2sumlem1  23591  mulog2sumlem3  23593  vmalogdivsum2  23595  selberg4lem1  23617  pntrlog2bndlem2  23635  pntrlog2bndlem4  23637  pntibndlem2  23648  pntlemr  23659  pntlemf  23662  pntlemo  23664  ragcom  23947  colperpexlem1  23976  lmiisolem  24033  hypcgrlem2  24037  brbtwn2  24080  colinearalglem1  24081  colinearalglem2  24082  axcontlem2  24140  axcontlem8  24146  clwlkisclwwlklem2a  24657  numclwwlk2  24979  grpoinvid2  25105  gxcom  25143  gxmodid  25153  ablodivdiv4  25165  vcoprne  25344  nvnncan  25430  smcnlem  25479  ipidsq  25495  ipasslem2  25619  minvecolem2  25663  hv2times  25850  pjhthlem1  26181  pjds3i  26503  ho2times  26610  opsqrlem6  26936  pjclem4  26990  pj3si  26998  csmdsymi  27125  ofoprabco  27377  fcnvgreu  27386  2sqmod  27509  qqhcn  27845  nnlogbexp  27893  esumpr2  27947  esumpfinval  27954  esumpfinvalf  27955  oddpwdcv  28167  eulerpartlemgs2  28192  fibp1  28213  orvcelval  28280  ballotlemscr  28330  ballotlemfrci  28339  signsplypnf  28380  lgamgulmlem2  28445  subfacp1lem5  28501  cvmliftlem10  28612  circum  28913  fallfacfwd  29133  faclimlem3  29145  fsumkthpow  29793  bpoly3  29795  bpoly4  29796  tan2h  30022  mblfinlem2  30027  itgaddnclem1  30048  itgmulc2nclem2  30057  areacirclem1  30082  areacirclem4  30085  istotbnd3  30242  iscringd  30371  diophin  30681  irrapxlem2  30734  pellexlem6  30745  pell1234qrmulcl  30766  rmxyval  30826  rmxyneg  30831  rmxyadd  30832  jm2.24  30876  jm2.25  30916  radcnvrat  31171  sub2times  31404  mul13d  31410  fperiodmullem  31452  fperiodmul  31453  isumneg  31516  climneg  31524  itgsinexp  31643  stoweidlem13  31684  stoweidlem42  31713  wallispilem4  31739  wallispilem5  31740  wallispi2lem1  31742  stirlinglem1  31745  stirlinglem3  31747  stirlinglem4  31748  stirlinglem5  31749  stirlinglem7  31751  stirlinglem10  31754  dirkertrigeqlem3  31771  fourierdlem30  31808  fourierdlem32  31810  fourierdlem42  31820  fourierdlem48  31826  fourierdlem49  31827  fourierdlem83  31861  sqwvfoura  31900  sqwvfourb  31901  sharhght  31920  rngcid  32527  ringcid  32570  lmodvsmdi  32710  dmatALTbas  32737  ldepsprlem  32808  sinhpcosh  32869  bj-bary1lem  34419  3atlem1  34947  pmod2iN  35313  polval2N  35370  lhple  35506  cdleme2  35693  cdleme35d  35918  cdleme42h  35948  cdlemeg46ngfr  35984  cdlemkid1  36388  lcfl7lem  36966  mapdpglem22  37160  mapdh6dN  37206  hdmap1l6d  37281  hdmapinvlem3  37390  snhesn  37496