Theorem 3eqtr2d 2203

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

Syntax hints:   → wi 4   = wceq 1342

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  fmptapd  5670  rdgisucinc  6344  ctm  7065  mulidnq  7321  ltrnqg  7352  recexprlem1ssl  7565  recexprlem1ssu  7566  ltmprr  7574  mulcmpblnrlemg  7672  caucvgsrlemoffcau  7730  negsub  8137  neg2sub  8149  divmuleqap  8604  divneg2ap  8623  qapne  9568  seqvalcd  10384  binom2  10555  bcpasc  10668  crim  10786  remullem  10799  max0addsup  11147  summodclem2a  11308  isum1p  11419  geo2sum  11441  cvgratz  11459  efi4p  11644  tanaddap  11666  addcos  11673  cos2tsin  11678  demoivreALT  11700  omeo  11820  sqgcd  11947  eulerthlemth  12141  pythagtriplem16  12188  fldivp1  12255  txrest  12817  limccnpcntop  13185  dvrecap  13218  cosq34lt1  13312