Theorem 3eqtr2d 2277

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  fmptapd  5906  rdgisucinc  6656  ctm  7449  mulidnq  7756  ltrnqg  7787  recexprlem1ssl  8000  recexprlem1ssu  8001  ltmprr  8009  mulcmpblnrlemg  8107  caucvgsrlemoffcau  8165  negsub  8575  neg2sub  8587  divmuleqap  9049  divneg2ap  9068  qapne  10048  seqvalcd  10911  binom2  11101  bcpasc  11218  hashf1lem2  11300  cats2catd  11555  crim  11637  remullem  11650  max0addsup  12000  summodclem2a  12164  isum1p  12275  geo2sum  12297  cvgratz  12315  efi4p  12500  tanaddap  12522  addcos  12529  cos2tsin  12534  demoivreALT  12557  omeo  12681  sqgcd  12822  eulerthlemth  13030  pythagtriplem16  13078  fldivp1  13147  pockthlem  13155  4sqlem10  13186  ballotfilemscr  13311  ballotfilemfrci  13320  ballotfilemfrceq  13321  gzsumval2  13763  grpinvid2  13907  imasgrp2  13962  mulgaddcomlem  13997  mulgmodid  14013  ablsubsub  14171  ablsubsub4  14172  gzsumsnfd  14196  opprunitd  14466  lmodfopne  14712  mpl0fi  15142  mplnegfi  15145  txrest  15426  limccnpcntop  15825  dvrecap  15863  dvply1  15915  cosq34lt1  16001  log2tlbndlog2  16139  birthdaylem2  16145  wilthlem1  16151  mersenne  16195  lgseisenlem1  16287  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem1  16298  2lgslem1  16308  qdiff  17196