Theorem 3eqtr2d 2270

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  fmptapd  5844  rdgisucinc  6550  ctm  7307  mulidnq  7608  ltrnqg  7639  recexprlem1ssl  7852  recexprlem1ssu  7853  ltmprr  7861  mulcmpblnrlemg  7959  caucvgsrlemoffcau  8017  negsub  8426  neg2sub  8438  divmuleqap  8896  divneg2ap  8915  qapne  9872  seqvalcd  10722  binom2  10912  bcpasc  11027  cats2catd  11349  crim  11418  remullem  11431  max0addsup  11779  summodclem2a  11941  isum1p  12052  geo2sum  12074  cvgratz  12092  efi4p  12277  tanaddap  12299  addcos  12306  cos2tsin  12311  demoivreALT  12334  omeo  12458  sqgcd  12599  eulerthlemth  12803  pythagtriplem16  12851  fldivp1  12920  pockthlem  12928  4sqlem10  12959  gsumval2  13479  grpinvid2  13635  imasgrp2  13696  mulgaddcomlem  13731  mulgmodid  13747  ablsubsub  13904  ablsubsub4  13905  gsumfzsnfd  13931  opprunitd  14123  lmodfopne  14339  mpl0fi  14715  mplnegfi  14718  txrest  14999  limccnpcntop  15398  dvrecap  15436  dvply1  15488  cosq34lt1  15573  wilthlem1  15703  mersenne  15720  lgseisenlem1  15798  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem1  15809  2lgslem1  15819