Theorem 3eqtr2d 2204

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

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  fmptapd  5676  rdgisucinc  6353  ctm  7074  mulidnq  7330  ltrnqg  7361  recexprlem1ssl  7574  recexprlem1ssu  7575  ltmprr  7583  mulcmpblnrlemg  7681  caucvgsrlemoffcau  7739  negsub  8146  neg2sub  8158  divmuleqap  8613  divneg2ap  8632  qapne  9577  seqvalcd  10394  binom2  10566  bcpasc  10679  crim  10800  remullem  10813  max0addsup  11161  summodclem2a  11322  isum1p  11433  geo2sum  11455  cvgratz  11473  efi4p  11658  tanaddap  11680  addcos  11687  cos2tsin  11692  demoivreALT  11714  omeo  11835  sqgcd  11962  eulerthlemth  12164  pythagtriplem16  12211  fldivp1  12278  pockthlem  12286  4sqlem10  12317  txrest  12916  limccnpcntop  13284  dvrecap  13317  cosq34lt1  13411