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  5684  rdgisucinc  6361  ctm  7082  mulidnq  7338  ltrnqg  7369  recexprlem1ssl  7582  recexprlem1ssu  7583  ltmprr  7591  mulcmpblnrlemg  7689  caucvgsrlemoffcau  7747  negsub  8154  neg2sub  8166  divmuleqap  8621  divneg2ap  8640  qapne  9585  seqvalcd  10402  binom2  10574  bcpasc  10687  crim  10809  remullem  10822  max0addsup  11170  summodclem2a  11331  isum1p  11442  geo2sum  11464  cvgratz  11482  efi4p  11667  tanaddap  11689  addcos  11696  cos2tsin  11701  demoivreALT  11723  omeo  11844  sqgcd  11971  eulerthlemth  12173  pythagtriplem16  12220  fldivp1  12287  pockthlem  12295  4sqlem10  12326  txrest  13029  limccnpcntop  13397  dvrecap  13430  cosq34lt1  13524