Theorem 3eqtr2d 2244

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  fmptapd  5777  rdgisucinc  6473  ctm  7213  mulidnq  7504  ltrnqg  7535  recexprlem1ssl  7748  recexprlem1ssu  7749  ltmprr  7757  mulcmpblnrlemg  7855  caucvgsrlemoffcau  7913  negsub  8322  neg2sub  8334  divmuleqap  8792  divneg2ap  8811  qapne  9762  seqvalcd  10608  binom2  10798  bcpasc  10913  crim  11202  remullem  11215  max0addsup  11563  summodclem2a  11725  isum1p  11836  geo2sum  11858  cvgratz  11876  efi4p  12061  tanaddap  12083  addcos  12090  cos2tsin  12095  demoivreALT  12118  omeo  12242  sqgcd  12383  eulerthlemth  12587  pythagtriplem16  12635  fldivp1  12704  pockthlem  12712  4sqlem10  12743  gsumval2  13262  grpinvid2  13418  imasgrp2  13479  mulgaddcomlem  13514  mulgmodid  13530  ablsubsub  13687  ablsubsub4  13688  gsumfzsnfd  13714  opprunitd  13905  lmodfopne  14121  mpl0fi  14497  mplnegfi  14500  txrest  14781  limccnpcntop  15180  dvrecap  15218  dvply1  15270  cosq34lt1  15355  wilthlem1  15485  mersenne  15502  lgseisenlem1  15580  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad2lem1  15591  2lgslem1  15601