Theorem 3eqtr2d 2498

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

Syntax hints:   -> wi 4   = wceq 1370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430

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

This theorem is referenced by:  fmptapd  6001  negsub  9758  neg2sub  9770  divmuleq  10137  divneg2  10156  discr  12102  bcpasc  12198  hashgval2  12243  hashf1lem2  12311  crim  12706  remullem  12719  incexclem  13401  isum1p  13406  geo2sum  13435  efi4p  13523  sinhval  13540  addcos  13560  cos2tsin  13565  demoivreALT  13587  rpnnen2lem11  13609  sadaddlem  13764  smumullem  13790  sqgcd  13844  eulerthlem2  13959  omeo  13983  pockthlem  14068  4sqlem10  14110  vdwlem2  14145  vdwlem6  14149  vdwlem8  14151  fuccocl  14976  resssetc  15062  resscatc  15075  uncfcurf  15151  yonedalem3b  15191  prdspjmhm  15597  grpinvid2  15689  imasgrp2  15772  lagsubg2  15844  cntzsubm  15955  sylow3lem2  16231  efgredleme  16344  ablsubsub  16411  ablsubsub4  16412  odadd2  16435  gex2abl  16437  pgpfac1lem3a  16682  abvneg  17025  lsppr  17280  psrass1  17584  resspsradd  17595  resspsrvsca  17597  mplcoe5  17655  mplcoe2OLD  17657  mplmon2mul  17690  evlslem2  17704  evlsvarsrng  17721  coe1tm  17834  ply1scl1  17853  evls1varsrng  17883  gzrngunit  17987  frlmsubgval  18301  frlmgsumOLD  18304  frlmgsum  18305  mamuass  18415  mavmulass  18471  mulmarep1gsum2  18496  mdetuni0  18543  maducoeval2  18562  madulid  18567  cmpfi  19127  cnconn  19142  txrest  19320  utopsnneiplem  19938  blcvx  20491  tchcphlem2  20867  minveclem2  21029  pjthlem1  21040  uniioovol  21175  uniioombllem2  21179  itg1addlem4  21293  mbfi1fseqlem5  21313  itg2mulc  21341  itg2monolem1  21344  itgaddlem1  21416  itgmulc2lem2  21426  dvrec  21545  lhop2  21603  ftc1lem5  21628  deg1submon1p  21740  plypf1  21796  coefv0  21831  coemulhi  21837  coemulc  21838  dgreq0  21848  dvply1  21866  vieta1  21894  aareccl  21908  aaliou3lem8  21927  dvtaylp  21951  mtest  21985  sineq0  22099  efif1olem2  22115  efif1olem4  22117  tanarg  22184  logtayl2  22223  isosctrlem2  22333  chordthmlem2  22344  chordthmlem4  22346  heron  22349  dcubic1lem  22354  dcubic1  22356  mcubic  22358  dquart  22364  quart1lem  22366  quart1  22367  efiasin  22399  asinsin  22403  atancj  22421  efiatan  22423  atanlogaddlem  22424  cosatan  22432  atantan  22434  atans2  22442  log2cnv  22455  log2tlbnd  22456  birthdaylem2  22462  cxplim  22481  wilthlem1  22522  basellem3  22536  musum  22647  musumsum  22648  muinv  22649  pclogsum  22670  mersenne  22682  dchrabs  22715  dchrinv  22716  lgseisenlem1  22804  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  lgsquad2lem1  22813  chebbnd1lem3  22836  chpchtlim  22844  rplogsumlem2  22850  dchrisumlem2  22855  dchrmusum2  22859  mulog2sumlem1  22899  mulog2sumlem3  22901  vmalogdivsum2  22903  selberg4lem1  22925  pntrlog2bndlem2  22943  pntrlog2bndlem4  22945  pntibndlem2  22956  pntlemr  22967  pntlemf  22970  pntlemo  22972  ragcom  23218  colperplem1  23240  brbtwn2  23286  colinearalglem1  23287  colinearalglem2  23288  axcontlem2  23346  axcontlem8  23352  grpoinvid2  23853  gxcom  23891  gxmodid  23901  ablodivdiv4  23913  vcoprne  24092  nvnncan  24178  smcnlem  24227  ipidsq  24243  ipasslem2  24367  minvecolem2  24411  hv2times  24598  pjhthlem1  24929  pjds3i  25251  ho2times  25358  opsqrlem6  25684  pjclem4  25738  pj3si  25746  csmdsymi  25873  ofoprabco  26116  fcnvgreu  26125  qqhcn  26554  nnlogbexp  26597  esumpr2  26651  esumpfinval  26658  esumpfinvalf  26659  oddpwdcv  26872  eulerpartlemgs2  26897  fibp1  26918  orvcelval  26985  ballotlemscr  27035  ballotlemfrci  27044  signsplypnf  27085  lgamgulmlem2  27150  subfacp1lem5  27206  cvmliftlem10  27317  fallfacfwd  27673  faclimlem3  27685  fsumkthpow  28333  bpoly3  28335  bpoly4  28336  tan2h  28562  mblfinlem2  28567  itgaddnclem1  28588  itgmulc2nclem2  28597  areacirclem1  28622  areacirclem4  28625  istotbnd3  28808  iscringd  28937  diophin  29249  irrapxlem2  29302  pellexlem6  29313  pell1234qrmulcl  29334  rmxyval  29394  rmxyadd  29400  jm2.24  29444  jm2.25  29486  isumneg  29913  climneg  29921  itgsinexp  29933  stoweidlem13  29946  stoweidlem42  29975  wallispilem4  30001  wallispilem5  30002  wallispi2lem1  30004  stirlinglem1  30007  stirlinglem3  30009  stirlinglem4  30010  stirlinglem5  30011  stirlinglem7  30013  stirlinglem10  30016  sharhght  30039  clwlkisclwwlklem2a  30585  numclwwlk2  30838  lmodvsmdi  30956  ldepsprlem  31113  mat2pmatmul  31194  pmatcollpw3lem  31237  pmattomply1mhmlem1  31273  sinhpcosh  31371  bj-bary1lem  32905  3atlem1  33433  pmod2iN  33799  polval2N  33856  lhple  33992  cdleme2  34178  cdleme35d  34402  cdleme42h  34432  cdlemeg46ngfr  34468  cdlemkid1  34872  lcfl7lem  35450  mapdpglem22  35644  mapdh6dN  35690  hdmap1l6d  35765  hdmapinvlem3  35874