Theorem 3eqtr2d 2273

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

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

This theorem is referenced by:  fmptapd  5880  rdgisucinc  6629  ctm  7413  mulidnq  7720  ltrnqg  7751  recexprlem1ssl  7964  recexprlem1ssu  7965  ltmprr  7973  mulcmpblnrlemg  8071  caucvgsrlemoffcau  8129  negsub  8537  neg2sub  8549  divmuleqap  9008  divneg2ap  9027  qapne  9989  seqvalcd  10847  binom2  11037  bcpasc  11153  cats2catd  11486  crim  11568  remullem  11581  max0addsup  11929  summodclem2a  12092  isum1p  12203  geo2sum  12225  cvgratz  12243  efi4p  12428  tanaddap  12450  addcos  12457  cos2tsin  12462  demoivreALT  12485  omeo  12609  sqgcd  12750  eulerthlemth  12954  pythagtriplem16  13002  fldivp1  13071  pockthlem  13079  4sqlem10  13110  ballotfilemscr  13206  ballotfilemfrci  13215  ballotfilemfrceq  13216  gsumval2  13660  grpinvid2  13808  imasgrp2  13863  mulgaddcomlem  13898  mulgmodid  13914  ablsubsub  14071  ablsubsub4  14072  gsumfzsnfd  14098  opprunitd  14355  lmodfopne  14600  mpl0fi  14983  mplnegfi  14986  txrest  15267  limccnpcntop  15666  dvrecap  15704  dvply1  15756  cosq34lt1  15841  wilthlem1  15974  mersenne  15991  lgseisenlem1  16069  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem1  16080  2lgslem1  16090  qdiff  16959