Theorem 3eqtr2d 2244

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  fmptapd  5775  rdgisucinc  6471  ctm  7211  mulidnq  7502  ltrnqg  7533  recexprlem1ssl  7746  recexprlem1ssu  7747  ltmprr  7755  mulcmpblnrlemg  7853  caucvgsrlemoffcau  7911  negsub  8320  neg2sub  8332  divmuleqap  8790  divneg2ap  8809  qapne  9760  seqvalcd  10606  binom2  10796  bcpasc  10911  crim  11169  remullem  11182  max0addsup  11530  summodclem2a  11692  isum1p  11803  geo2sum  11825  cvgratz  11843  efi4p  12028  tanaddap  12050  addcos  12057  cos2tsin  12062  demoivreALT  12085  omeo  12209  sqgcd  12350  eulerthlemth  12554  pythagtriplem16  12602  fldivp1  12671  pockthlem  12679  4sqlem10  12710  gsumval2  13229  grpinvid2  13385  imasgrp2  13446  mulgaddcomlem  13481  mulgmodid  13497  ablsubsub  13654  ablsubsub4  13655  gsumfzsnfd  13681  opprunitd  13872  lmodfopne  14088  mpl0fi  14464  mplnegfi  14467  txrest  14748  limccnpcntop  15147  dvrecap  15185  dvply1  15237  cosq34lt1  15322  wilthlem1  15452  mersenne  15469  lgseisenlem1  15547  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  2lgslem1  15568