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  5708  rdgisucinc  6386  ctm  7108  mulidnq  7388  ltrnqg  7419  recexprlem1ssl  7632  recexprlem1ssu  7633  ltmprr  7641  mulcmpblnrlemg  7739  caucvgsrlemoffcau  7797  negsub  8205  neg2sub  8217  divmuleqap  8674  divneg2ap  8693  qapne  9639  seqvalcd  10459  binom2  10632  bcpasc  10746  crim  10867  remullem  10880  max0addsup  11228  summodclem2a  11389  isum1p  11500  geo2sum  11522  cvgratz  11540  efi4p  11725  tanaddap  11747  addcos  11754  cos2tsin  11759  demoivreALT  11781  omeo  11903  sqgcd  12030  eulerthlemth  12232  pythagtriplem16  12279  fldivp1  12346  pockthlem  12354  4sqlem10  12385  grpinvid2  12925  mulgaddcomlem  13006  mulgmodid  13022  ablsubsub  13121  ablsubsub4  13122  opprunitd  13279  lmodfopne  13416  txrest  13779  limccnpcntop  14147  dvrecap  14180  cosq34lt1  14274  lgseisenlem1  14453