Theorem 3eqtr2d 2235

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fmptapd  5753  rdgisucinc  6443  ctm  7175  mulidnq  7456  ltrnqg  7487  recexprlem1ssl  7700  recexprlem1ssu  7701  ltmprr  7709  mulcmpblnrlemg  7807  caucvgsrlemoffcau  7865  negsub  8274  neg2sub  8286  divmuleqap  8744  divneg2ap  8763  qapne  9713  seqvalcd  10553  binom2  10743  bcpasc  10858  crim  11023  remullem  11036  max0addsup  11384  summodclem2a  11546  isum1p  11657  geo2sum  11679  cvgratz  11697  efi4p  11882  tanaddap  11904  addcos  11911  cos2tsin  11916  demoivreALT  11939  omeo  12063  sqgcd  12196  eulerthlemth  12400  pythagtriplem16  12448  fldivp1  12517  pockthlem  12525  4sqlem10  12556  gsumval2  13040  grpinvid2  13185  imasgrp2  13240  mulgaddcomlem  13275  mulgmodid  13291  ablsubsub  13448  ablsubsub4  13449  gsumfzsnfd  13475  opprunitd  13666  lmodfopne  13882  txrest  14512  limccnpcntop  14911  dvrecap  14949  dvply1  15001  cosq34lt1  15086  wilthlem1  15216  mersenne  15233  lgseisenlem1  15311  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  2lgslem1  15332