Theorem 3eqtr2d 2246

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 2243	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtrd 2240	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  fmptapd  5798  rdgisucinc  6494  ctm  7237  mulidnq  7537  ltrnqg  7568  recexprlem1ssl  7781  recexprlem1ssu  7782  ltmprr  7790  mulcmpblnrlemg  7888  caucvgsrlemoffcau  7946  negsub  8355  neg2sub  8367  divmuleqap  8825  divneg2ap  8844  qapne  9795  seqvalcd  10643  binom2  10833  bcpasc  10948  crim  11284  remullem  11297  max0addsup  11645  summodclem2a  11807  isum1p  11918  geo2sum  11940  cvgratz  11958  efi4p  12143  tanaddap  12165  addcos  12172  cos2tsin  12177  demoivreALT  12200  omeo  12324  sqgcd  12465  eulerthlemth  12669  pythagtriplem16  12717  fldivp1  12786  pockthlem  12794  4sqlem10  12825  gsumval2  13344  grpinvid2  13500  imasgrp2  13561  mulgaddcomlem  13596  mulgmodid  13612  ablsubsub  13769  ablsubsub4  13770  gsumfzsnfd  13796  opprunitd  13987  lmodfopne  14203  mpl0fi  14579  mplnegfi  14582  txrest  14863  limccnpcntop  15262  dvrecap  15300  dvply1  15352  cosq34lt1  15437  wilthlem1  15567  mersenne  15584  lgseisenlem1  15662  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem1  15673  2lgslem1  15683