Theorem 3eqtr2d 2216

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

Syntax hints:   → wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  fmptapd  5709  rdgisucinc  6388  ctm  7110  mulidnq  7390  ltrnqg  7421  recexprlem1ssl  7634  recexprlem1ssu  7635  ltmprr  7643  mulcmpblnrlemg  7741  caucvgsrlemoffcau  7799  negsub  8207  neg2sub  8219  divmuleqap  8676  divneg2ap  8695  qapne  9641  seqvalcd  10461  binom2  10634  bcpasc  10748  crim  10869  remullem  10882  max0addsup  11230  summodclem2a  11391  isum1p  11502  geo2sum  11524  cvgratz  11542  efi4p  11727  tanaddap  11749  addcos  11756  cos2tsin  11761  demoivreALT  11783  omeo  11905  sqgcd  12032  eulerthlemth  12234  pythagtriplem16  12281  fldivp1  12348  pockthlem  12356  4sqlem10  12387  grpinvid2  12930  mulgaddcomlem  13011  mulgmodid  13027  ablsubsub  13126  ablsubsub4  13127  opprunitd  13284  lmodfopne  13421  txrest  13815  limccnpcntop  14183  dvrecap  14216  cosq34lt1  14310  lgseisenlem1  14489