Theorem 3eqtr2d 2442

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

Syntax hints:   -> wi 4   = wceq 1649

This theorem is referenced by:  negsub  9305  neg2sub  9317  divmuleq  9675  divneg2  9694  discr  11471  bcpasc  11567  hashgval2  11607  hashf1lem2  11660  crim  11875  remullem  11888  incexclem  12571  isum1p  12576  geo2sum  12605  efi4p  12693  sinhval  12710  addcos  12730  cos2tsin  12735  demoivreALT  12757  rpnnen2lem11  12779  sadaddlem  12933  smumullem  12959  sqgcd  13013  eulerthlem2  13126  omeo  13143  pockthlem  13228  4sqlem10  13270  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  fuccocl  14116  resssetc  14202  resscatc  14215  uncfcurf  14291  yonedalem3b  14331  prdspjmhm  14721  grpinvid2  14809  imasgrp2  14888  lagsubg2  14956  cntzsubm  15089  sylow3lem2  15217  efgredleme  15330  ablsubsub  15397  ablsubsub4  15398  odadd2  15419  gex2abl  15421  pgpfac1lem3a  15589  abvneg  15877  lsppr  16120  psrass1  16424  resspsradd  16434  resspsrvsca  16436  mplcoe2  16485  mplmon2mul  16516  evlslem2  16523  coe1tm  16620  ply1scl1  16638  gzrngunit  16719  cmpfi  17425  cnconn  17438  txrest  17616  utopsnneiplem  18230  blcvx  18782  tchcphlem2  19146  minveclem2  19280  pjthlem1  19291  uniioovol  19424  uniioombllem2  19428  itg1addlem4  19544  mbfi1fseqlem5  19564  itg2mulc  19592  itg2monolem1  19595  itgaddlem1  19667  itgmulc2lem2  19677  dvrec  19794  lhop2  19852  ftc1lem5  19877  deg1submon1p  20028  plypf1  20084  coefv0  20119  coemulhi  20125  coemulc  20126  dgreq0  20136  dvply1  20154  vieta1  20182  aareccl  20196  aaliou3lem8  20215  dvtaylp  20239  mtest  20273  sineq0  20382  efif1olem2  20398  efif1olem4  20400  tanarg  20467  logtayl2  20506  isosctrlem2  20616  chordthmlem2  20627  chordthmlem4  20629  dcubic1lem  20636  dcubic1  20638  mcubic  20640  dquart  20646  quart1lem  20648  quart1  20649  efiasin  20681  asinsin  20685  atancj  20703  efiatan  20705  atanlogaddlem  20706  cosatan  20714  atantan  20716  atans2  20724  log2cnv  20737  log2tlbnd  20738  birthdaylem2  20744  cxplim  20763  wilthlem1  20804  basellem3  20818  musum  20929  musumsum  20930  muinv  20931  pclogsum  20952  mersenne  20964  dchrabs  20997  dchrinv  20998  lgseisenlem1  21086  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad2lem1  21095  chebbnd1lem3  21118  chpchtlim  21126  rplogsumlem2  21132  dchrisumlem2  21137  dchrmusum2  21141  mulog2sumlem1  21181  mulog2sumlem3  21183  vmalogdivsum2  21185  selberg4lem1  21207  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  pntibndlem2  21238  pntlemr  21249  pntlemf  21252  pntlemo  21254  grpoinvid2  21772  gxcom  21810  gxmodid  21820  ablodivdiv4  21832  vcoprne  22011  nvnncan  22097  smcnlem  22146  ipidsq  22162  ipasslem2  22286  minvecolem2  22330  hv2times  22516  pjhthlem1  22846  pjds3i  23168  ho2times  23275  opsqrlem6  23601  pjclem4  23655  pj3si  23663  csmdsymi  23790  fmptapd  24014  ofoprabco  24032  qqhcn  24328  nnlogbexp  24357  esumpr2  24411  esumpfinval  24418  esumpfinvalf  24419  orvcelval  24679  ballotlemscr  24729  ballotlemfrci  24738  lgamgulmlem2  24767  subfacp1lem5  24823  cvmliftlem10  24934  fallfacfwd  25303  faclimlem3  25312  brbtwn2  25748  colinearalglem1  25749  colinearalglem2  25750  axcontlem2  25808  axcontlem8  25814  fsumkthpow  26006  bpoly3  26008  bpoly4  26009  mblfinlem  26143  itgaddnclem1  26162  itgmulc2nclem2  26171  areacirclem2  26181  areacirclem5  26185  istotbnd3  26370  iscringd  26499  diophin  26721  irrapxlem2  26776  pellexlem6  26787  pell1234qrmulcl  26808  rmxyval  26868  rmxyadd  26874  jm2.24  26918  jm2.25  26960  frlmgsum  27100  mamuass  27328  isumneg  27595  climneg  27603  itgsinexp  27616  stoweidlem13  27629  stoweidlem42  27658  wallispilem4  27684  wallispilem5  27685  wallispi2lem1  27687  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem7  27696  stirlinglem10  27699  sharhght  27722  sinhpcosh  28197  3atlem1  29965  pmod2iN  30331  polval2N  30388  lhple  30524  cdleme2  30710  cdleme35d  30934  cdleme42h  30964  cdlemeg46ngfr  31000  cdlemkid1  31404  lcfl7lem  31982  mapdpglem22  32176  mapdh6dN  32222  hdmap1l6d  32297  hdmapinvlem3  32406

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397