Theorem 3eqtr2d 2209

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr2d.2	⊢ (𝜑 → 𝐶 = 𝐵)
3eqtr2d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtr2d	⊢ (𝜑 → 𝐴 = 𝐷)

Proof of Theorem 3eqtr2d

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	1, 2	eqtr4d 2206	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2203	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  fmptapd  5687  rdgisucinc  6364  ctm  7086  mulidnq  7351  ltrnqg  7382  recexprlem1ssl  7595  recexprlem1ssu  7596  ltmprr  7604  mulcmpblnrlemg  7702  caucvgsrlemoffcau  7760  negsub  8167  neg2sub  8179  divmuleqap  8634  divneg2ap  8653  qapne  9598  seqvalcd  10415  binom2  10587  bcpasc  10700  crim  10822  remullem  10835  max0addsup  11183  summodclem2a  11344  isum1p  11455  geo2sum  11477  cvgratz  11495  efi4p  11680  tanaddap  11702  addcos  11709  cos2tsin  11714  demoivreALT  11736  omeo  11857  sqgcd  11984  eulerthlemth  12186  pythagtriplem16  12233  fldivp1  12300  pockthlem  12308  4sqlem10  12339  grpinvid2  12755  txrest  13070  limccnpcntop  13438  dvrecap  13471  cosq34lt1  13565