Theorem 3eqtr2d 2228

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 2225	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtrd 2222	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  fmptapd  5728  rdgisucinc  6411  ctm  7139  mulidnq  7419  ltrnqg  7450  recexprlem1ssl  7663  recexprlem1ssu  7664  ltmprr  7672  mulcmpblnrlemg  7770  caucvgsrlemoffcau  7828  negsub  8236  neg2sub  8248  divmuleqap  8705  divneg2ap  8724  qapne  9671  seqvalcd  10492  binom2  10666  bcpasc  10781  crim  10902  remullem  10915  max0addsup  11263  summodclem2a  11424  isum1p  11535  geo2sum  11557  cvgratz  11575  efi4p  11760  tanaddap  11782  addcos  11789  cos2tsin  11794  demoivreALT  11816  omeo  11938  sqgcd  12065  eulerthlemth  12267  pythagtriplem16  12314  fldivp1  12383  pockthlem  12391  4sqlem10  12422  gsumval2  12875  grpinvid2  13012  imasgrp2  13067  mulgaddcomlem  13102  mulgmodid  13118  ablsubsub  13274  ablsubsub4  13275  opprunitd  13477  lmodfopne  13659  txrest  14253  limccnpcntop  14621  dvrecap  14654  cosq34lt1  14748  wilthlem1  14875  lgseisenlem1  14928