Theorem 3eqtr2d 2178

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 2175	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2172	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  fmptapd  5611  rdgisucinc  6282  ctm  6994  mulidnq  7197  ltrnqg  7228  recexprlem1ssl  7441  recexprlem1ssu  7442  ltmprr  7450  mulcmpblnrlemg  7548  caucvgsrlemoffcau  7606  negsub  8010  neg2sub  8022  divmuleqap  8477  divneg2ap  8496  qapne  9431  seqvalcd  10232  binom2  10403  bcpasc  10512  crim  10630  remullem  10643  max0addsup  10991  summodclem2a  11150  isum1p  11261  geo2sum  11283  cvgratz  11301  efi4p  11424  tanaddap  11446  addcos  11453  cos2tsin  11458  demoivreALT  11480  omeo  11595  sqgcd  11717  txrest  12445  limccnpcntop  12813  dvrecap  12846  cosq34lt1  12931