Theorem 3eqtrrd 2203

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

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  nnanq0  7395  1idprl  7527  1idpru  7528  axcnre  7818  fseq1p1m1  10025  expmulzap  10497  expubnd  10508  subsq  10557  bcm1k  10669  bcpasc  10675  crim  10796  rereb  10801  fsumparts  11407  isumshft  11427  geosergap  11443  efsub  11618  sincossq  11685  efieq1re  11708  bezoutlema  11928  bezoutlemb  11929  eucalg  11987  phiprmpw  12150  modprmn0modprm0  12184  coprimeprodsq  12185  pythagtriplem15  12206  pythagtriplem17  12208  fldivp1  12274  1arithlem4  12292  strsetsid  12423  setsslid  12440  upxp  12872  uptx  12874  lgsdilem  13528  2sqlem3  13553