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  8574  neg2sub  8586  divmuleqap  9047  divneg2ap  9066  qapne  10039  seqvalcd  10898  binom2  11088  bcpasc  11204  hashf1lem2  11286  cats2catd  11541  crim  11623  remullem  11636  max0addsup  11985  summodclem2a  12148  isum1p  12259  geo2sum  12281  cvgratz  12299  efi4p  12484  tanaddap  12506  addcos  12513  cos2tsin  12518  demoivreALT  12541  omeo  12665  sqgcd  12806  eulerthlemth  13010  pythagtriplem16  13058  fldivp1  13127  pockthlem  13135  4sqlem10  13166  ballotfilemscr  13262  ballotfilemfrci  13271  ballotfilemfrceq  13272  gzsumval2  13714  grpinvid2  13858  imasgrp2  13913  mulgaddcomlem  13948  mulgmodid  13964  ablsubsub  14122  ablsubsub4  14123  gzsumsnfd  14147  opprunitd  14417  lmodfopne  14663  mpl0fi  15093  mplnegfi  15096  txrest  15377  limccnpcntop  15776  dvrecap  15814  dvply1  15866  cosq34lt1  15951  log2tlbndlog2  16082  birthdaylem2  16088  wilthlem1  16094  mersenne  16111  lgseisenlem1  16189  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem1  16200  2lgslem1  16210  qdiff  17098