Theorem 3eqtr2d 2270

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  fmptapd  5845  rdgisucinc  6551  ctm  7308  mulidnq  7609  ltrnqg  7640  recexprlem1ssl  7853  recexprlem1ssu  7854  ltmprr  7862  mulcmpblnrlemg  7960  caucvgsrlemoffcau  8018  negsub  8427  neg2sub  8439  divmuleqap  8897  divneg2ap  8916  qapne  9873  seqvalcd  10724  binom2  10914  bcpasc  11029  cats2catd  11354  crim  11436  remullem  11449  max0addsup  11797  summodclem2a  11960  isum1p  12071  geo2sum  12093  cvgratz  12111  efi4p  12296  tanaddap  12318  addcos  12325  cos2tsin  12330  demoivreALT  12353  omeo  12477  sqgcd  12618  eulerthlemth  12822  pythagtriplem16  12870  fldivp1  12939  pockthlem  12947  4sqlem10  12978  gsumval2  13498  grpinvid2  13654  imasgrp2  13715  mulgaddcomlem  13750  mulgmodid  13766  ablsubsub  13923  ablsubsub4  13924  gsumfzsnfd  13950  opprunitd  14143  lmodfopne  14359  mpl0fi  14735  mplnegfi  14738  txrest  15019  limccnpcntop  15418  dvrecap  15456  dvply1  15508  cosq34lt1  15593  wilthlem1  15723  mersenne  15740  lgseisenlem1  15818  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem1  15829  2lgslem1  15839  qdiff  16704