Theorem 3eqtr2d 2268

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  fmptapd  5830  rdgisucinc  6531  ctm  7276  mulidnq  7576  ltrnqg  7607  recexprlem1ssl  7820  recexprlem1ssu  7821  ltmprr  7829  mulcmpblnrlemg  7927  caucvgsrlemoffcau  7985  negsub  8394  neg2sub  8406  divmuleqap  8864  divneg2ap  8883  qapne  9834  seqvalcd  10683  binom2  10873  bcpasc  10988  cats2catd  11301  crim  11369  remullem  11382  max0addsup  11730  summodclem2a  11892  isum1p  12003  geo2sum  12025  cvgratz  12043  efi4p  12228  tanaddap  12250  addcos  12257  cos2tsin  12262  demoivreALT  12285  omeo  12409  sqgcd  12550  eulerthlemth  12754  pythagtriplem16  12802  fldivp1  12871  pockthlem  12879  4sqlem10  12910  gsumval2  13430  grpinvid2  13586  imasgrp2  13647  mulgaddcomlem  13682  mulgmodid  13698  ablsubsub  13855  ablsubsub4  13856  gsumfzsnfd  13882  opprunitd  14074  lmodfopne  14290  mpl0fi  14666  mplnegfi  14669  txrest  14950  limccnpcntop  15349  dvrecap  15387  dvply1  15439  cosq34lt1  15524  wilthlem1  15654  mersenne  15671  lgseisenlem1  15749  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad2lem1  15760  2lgslem1  15770