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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  nnanq0  7721  1idprl  7853  1idpru  7854  axcnre  8144  fseq1p1m1  10374  seqf1oglem1  10827  expmulzap  10893  expubnd  10904  subsq  10954  bcm1k  11068  bcpasc  11074  crim  11481  rereb  11486  fsumparts  12094  isumshft  12114  geosergap  12130  efsub  12305  sincossq  12372  efieq1re  12396  bezoutlema  12633  bezoutlemb  12634  eucalg  12694  phiprmpw  12857  modprmn0modprm0  12892  coprimeprodsq  12893  pythagtriplem15  12914  pythagtriplem17  12916  fldivp1  12984  1arithlem4  13002  strsetsid  13178  setsslid  13196  pwsbas  13438  opprunitd  14188  cnfldsub  14654  upxp  15066  uptx  15068  perfectlem2  15797  lgsdilem  15829  gausslemma2dlem1a  15860  2sqlem3  15919