Theorem 3eqtr2d 2429

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

Syntax hints:   -> wi 4   = wceq 1399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360

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

This theorem is referenced by:  fmptapd  5997  negsub  9780  neg2sub  9792  divmuleq  10166  divneg2  10185  discr  12205  bcpasc  12301  hashgval2  12349  hashf1lem2  12409  relexpaddnn  12886  crim  12950  remullem  12963  incexclem  13650  isum1p  13655  geo2sum  13684  efi4p  13874  sinhval  13891  addcos  13911  cos2tsin  13916  demoivreALT  13938  rpnnen2lem11  13960  sadaddlem  14118  smumullem  14144  sqgcd  14198  eulerthlem2  14314  omeo  14340  pockthlem  14425  4sqlem10  14467  vdwlem2  14502  vdwlem6  14506  vdwlem8  14508  fuccocl  15370  resssetc  15488  resscatc  15501  uncfcurf  15625  yonedalem3b  15665  prdspjmhm  16115  grpinvid2  16216  imasgrp2  16302  lagsubg2  16379  cntzsubm  16490  sylow3lem2  16765  efgredleme  16878  ablsubsub  16945  ablsubsub4  16946  odadd2  16972  gex2abl  16974  pgpfac1lem3a  17240  abvneg  17596  lsppr  17852  psrass1  18173  resspsradd  18184  resspsrvsca  18186  mplcoe5  18244  mplcoe2OLD  18246  mplmon2mul  18279  evlslem2  18293  evlsvarsrng  18310  coe1tm  18427  ply1scl1  18446  evls1varsrng  18489  gzrngunit  18596  frlmsubgval  18887  frlmgsumOLD  18890  frlmgsum  18891  mamuass  18989  mavmulass  19136  mulmarep1gsum2  19161  mdetuni0  19208  maducoeval2  19227  madulid  19232  mat2pmatmul  19317  decpmatmulsumfsupp  19359  pmatcollpwlem  19366  pm2mpmhmlem1  19404  cmpfi  19994  cnconn  20008  txrest  20217  utopsnneiplem  20835  blcvx  21388  tchcphlem2  21764  minveclem2  21926  pjthlem1  21937  uniioovol  22073  uniioombllem2  22077  itg1addlem4  22191  mbfi1fseqlem5  22211  itg2mulc  22239  itg2monolem1  22242  itgaddlem1  22314  itgmulc2lem2  22324  dvrec  22443  lhop2  22501  ftc1lem5  22526  deg1submon1p  22638  plypf1  22694  coefv0  22730  coemulhi  22736  coemulc  22737  dgreq0  22747  dvply1  22765  vieta1  22793  aareccl  22807  aaliou3lem8  22826  dvtaylp  22850  mtest  22884  sineq0  22999  efif1olem2  23015  efif1olem4  23017  tanarg  23091  logtayl2  23130  nnlogbexp  23239  isosctrlem2  23269  chordthmlem2  23280  chordthmlem4  23282  heron  23285  dcubic1lem  23290  dcubic1  23292  mcubic  23294  dquart  23300  quart1lem  23302  quart1  23303  efiasin  23335  asinsin  23339  atancj  23357  efiatan  23359  atanlogaddlem  23360  cosatan  23368  atantan  23370  atans2  23378  log2cnv  23391  log2tlbnd  23392  birthdaylem2  23399  cxplim  23418  wilthlem1  23459  basellem3  23473  musum  23584  musumsum  23585  muinv  23586  pclogsum  23607  mersenne  23619  dchrabs  23652  dchrinv  23653  lgseisenlem1  23741  lgsquadlem1  23746  lgsquadlem2  23747  lgsquadlem3  23748  lgsquad2lem1  23750  chebbnd1lem3  23773  chpchtlim  23781  rplogsumlem2  23787  dchrisumlem2  23792  dchrmusum2  23796  mulog2sumlem1  23836  mulog2sumlem3  23838  vmalogdivsum2  23840  selberg4lem1  23862  pntrlog2bndlem2  23880  pntrlog2bndlem4  23882  pntibndlem2  23893  pntlemr  23904  pntlemf  23907  pntlemo  23909  ragcom  24195  colperpexlem1  24224  lmiisolem  24281  hypcgrlem2  24285  brbtwn2  24329  colinearalglem1  24330  colinearalglem2  24331  axcontlem2  24389  axcontlem8  24395  clwlkisclwwlklem2a  24906  numclwwlk2  25228  grpoinvid2  25350  gxcom  25388  gxmodid  25398  ablodivdiv4  25410  vcoprne  25589  nvnncan  25675  smcnlem  25724  ipidsq  25740  ipasslem2  25864  minvecolem2  25908  hv2times  26095  pjhthlem1  26426  pjds3i  26748  ho2times  26854  opsqrlem6  27180  pjclem4  27234  pj3si  27242  csmdsymi  27369  ofoprabco  27651  fcnvgreu  27660  2sqmod  27789  qqhcn  28125  esumpr2  28215  esumpfinval  28223  esumpfinvalf  28224  carsggect  28445  oddpwdcv  28477  eulerpartlemgs2  28502  fibp1  28523  orvcelval  28590  ballotlemscr  28640  ballotlemfrci  28649  signsplypnf  28690  lgamgulmlem2  28761  subfacp1lem5  28817  cvmliftlem10  28928  circum  29229  fallfacfwd  29324  faclimlem3  29336  fsumkthpow  29971  bpoly3  29973  bpoly4  29974  tan2h  30212  mblfinlem2  30217  itgaddnclem1  30239  itgmulc2nclem2  30248  areacirclem1  30273  areacirclem4  30276  istotbnd3  30433  iscringd  30562  diophin  30871  irrapxlem2  30924  pellexlem6  30935  pell1234qrmulcl  30956  rmxyval  31016  rmxyneg  31021  rmxyadd  31022  jm2.24  31066  jm2.25  31107  radcnvrat  31363  binomcxplemnotnn0  31429  sub2times  31622  mul13d  31628  fperiodmullem  31669  fperiodmul  31670  isumneg  31774  climneg  31782  itgsinexp  31919  stoweidlem13  31961  stoweidlem42  31990  wallispilem4  32016  wallispilem5  32017  wallispi2lem1  32019  stirlinglem1  32022  stirlinglem3  32024  stirlinglem4  32025  stirlinglem5  32026  stirlinglem7  32028  stirlinglem10  32031  dirkertrigeqlem3  32048  fourierdlem30  32085  fourierdlem32  32087  fourierdlem42  32097  fourierdlem48  32103  fourierdlem49  32104  fourierdlem83  32138  sqwvfoura  32177  sqwvfourb  32178  etransclem2  32185  etransclem46  32229  sharhght  32248  rngcid  32987  ringcid  33033  lmodvsmdi  33175  dmatALTbas  33202  ldepsprlem  33273  sinhpcosh  33470  bj-bary1lem  35023  3atlem1  35620  pmod2iN  35986  polval2N  36043  lhple  36179  cdleme2  36366  cdleme35d  36591  cdleme42h  36621  cdlemeg46ngfr  36657  cdlemkid1  37061  lcfl7lem  37639  mapdpglem22  37833  mapdh6dN  37879  hdmap1l6d  37954  hdmapinvlem3  38063  snhesn  38281