Theorem 3eqtr2d 2133

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

Syntax hints:   → wi 4   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

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

This theorem is referenced by:  fmptapd  5527  rdgisucinc  6188  ctm  6871  mulidnq  7045  ltrnqg  7076  recexprlem1ssl  7289  recexprlem1ssu  7290  ltmprr  7298  mulcmpblnrlemg  7383  caucvgsrlemoffcau  7440  negsub  7827  neg2sub  7839  divmuleqap  8281  divneg2ap  8300  qapne  9223  binom2  10180  bcpasc  10289  crim  10407  remullem  10420  max0addsup  10767  summodclem2a  10924  isum1p  11035  geo2sum  11057  cvgratz  11075  efi4p  11157  tanaddap  11179  addcos  11186  cos2tsin  11191  demoivreALT  11212  omeo  11325  sqgcd  11445