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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  fmptapd  5853  rdgisucinc  6594  ctm  7368  mulidnq  7669  ltrnqg  7700  recexprlem1ssl  7913  recexprlem1ssu  7914  ltmprr  7922  mulcmpblnrlemg  8020  caucvgsrlemoffcau  8078  negsub  8486  neg2sub  8498  divmuleqap  8956  divneg2ap  8975  qapne  9934  seqvalcd  10786  binom2  10976  bcpasc  11091  cats2catd  11416  crim  11498  remullem  11511  max0addsup  11859  summodclem2a  12022  isum1p  12133  geo2sum  12155  cvgratz  12173  efi4p  12358  tanaddap  12380  addcos  12387  cos2tsin  12392  demoivreALT  12415  omeo  12539  sqgcd  12680  eulerthlemth  12884  pythagtriplem16  12932  fldivp1  13001  pockthlem  13009  4sqlem10  13040  gsumval2  13560  grpinvid2  13716  imasgrp2  13777  mulgaddcomlem  13812  mulgmodid  13828  ablsubsub  13985  ablsubsub4  13986  gsumfzsnfd  14012  opprunitd  14205  lmodfopne  14422  mpl0fi  14803  mplnegfi  14806  txrest  15087  limccnpcntop  15486  dvrecap  15524  dvply1  15576  cosq34lt1  15661  wilthlem1  15794  mersenne  15811  lgseisenlem1  15889  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad2lem1  15900  2lgslem1  15910  qdiff  16781