Theorem 3eqtrrd 2208

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  nnanq0  7420  1idprl  7552  1idpru  7553  axcnre  7843  fseq1p1m1  10050  expmulzap  10522  expubnd  10533  subsq  10582  bcm1k  10694  bcpasc  10700  crim  10822  rereb  10827  fsumparts  11433  isumshft  11453  geosergap  11469  efsub  11644  sincossq  11711  efieq1re  11734  bezoutlema  11954  bezoutlemb  11955  eucalg  12013  phiprmpw  12176  modprmn0modprm0  12210  coprimeprodsq  12211  pythagtriplem15  12232  pythagtriplem17  12234  fldivp1  12300  1arithlem4  12318  strsetsid  12449  setsslid  12466  upxp  13066  uptx  13068  lgsdilem  13722  2sqlem3  13747