Theorem 3eqtrrd 2269

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)
3eqtrd.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtrrd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtrrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	eqtrd 2264	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2265	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:  nnanq0  7678  1idprl  7810  1idpru  7811  axcnre  8101  fseq1p1m1  10329  seqf1oglem1  10782  expmulzap  10848  expubnd  10859  subsq  10909  bcm1k  11023  bcpasc  11029  crim  11436  rereb  11441  fsumparts  12049  isumshft  12069  geosergap  12085  efsub  12260  sincossq  12327  efieq1re  12351  bezoutlema  12588  bezoutlemb  12589  eucalg  12649  phiprmpw  12812  modprmn0modprm0  12847  coprimeprodsq  12848  pythagtriplem15  12869  pythagtriplem17  12871  fldivp1  12939  1arithlem4  12957  strsetsid  13133  setsslid  13151  pwsbas  13393  opprunitd  14143  cnfldsub  14608  upxp  15015  uptx  15017  perfectlem2  15743  lgsdilem  15775  gausslemma2dlem1a  15806  2sqlem3  15865