Theorem 3eqtr2d 2235

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fmptapd  5756  rdgisucinc  6452  ctm  7184  mulidnq  7473  ltrnqg  7504  recexprlem1ssl  7717  recexprlem1ssu  7718  ltmprr  7726  mulcmpblnrlemg  7824  caucvgsrlemoffcau  7882  negsub  8291  neg2sub  8303  divmuleqap  8761  divneg2ap  8780  qapne  9730  seqvalcd  10570  binom2  10760  bcpasc  10875  crim  11040  remullem  11053  max0addsup  11401  summodclem2a  11563  isum1p  11674  geo2sum  11696  cvgratz  11714  efi4p  11899  tanaddap  11921  addcos  11928  cos2tsin  11933  demoivreALT  11956  omeo  12080  sqgcd  12221  eulerthlemth  12425  pythagtriplem16  12473  fldivp1  12542  pockthlem  12550  4sqlem10  12581  gsumval2  13099  grpinvid2  13255  imasgrp2  13316  mulgaddcomlem  13351  mulgmodid  13367  ablsubsub  13524  ablsubsub4  13525  gsumfzsnfd  13551  opprunitd  13742  lmodfopne  13958  txrest  14596  limccnpcntop  14995  dvrecap  15033  dvply1  15085  cosq34lt1  15170  wilthlem1  15300  mersenne  15317  lgseisenlem1  15395  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem1  15406  2lgslem1  15416