Theorem 3eqtr2d 2268

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

Syntax hints:   -> wi 4   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  fmptapd  5834  rdgisucinc  6537  ctm  7287  mulidnq  7587  ltrnqg  7618  recexprlem1ssl  7831  recexprlem1ssu  7832  ltmprr  7840  mulcmpblnrlemg  7938  caucvgsrlemoffcau  7996  negsub  8405  neg2sub  8417  divmuleqap  8875  divneg2ap  8894  qapne  9846  seqvalcd  10695  binom2  10885  bcpasc  11000  cats2catd  11317  crim  11385  remullem  11398  max0addsup  11746  summodclem2a  11908  isum1p  12019  geo2sum  12041  cvgratz  12059  efi4p  12244  tanaddap  12266  addcos  12273  cos2tsin  12278  demoivreALT  12301  omeo  12425  sqgcd  12566  eulerthlemth  12770  pythagtriplem16  12818  fldivp1  12887  pockthlem  12895  4sqlem10  12926  gsumval2  13446  grpinvid2  13602  imasgrp2  13663  mulgaddcomlem  13698  mulgmodid  13714  ablsubsub  13871  ablsubsub4  13872  gsumfzsnfd  13898  opprunitd  14090  lmodfopne  14306  mpl0fi  14682  mplnegfi  14685  txrest  14966  limccnpcntop  15365  dvrecap  15403  dvply1  15455  cosq34lt1  15540  wilthlem1  15670  mersenne  15687  lgseisenlem1  15765  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad2lem1  15776  2lgslem1  15786