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  7677  1idprl  7809  1idpru  7810  axcnre  8100  fseq1p1m1  10328  seqf1oglem1  10780  expmulzap  10846  expubnd  10857  subsq  10907  bcm1k  11021  bcpasc  11027  crim  11418  rereb  11423  fsumparts  12030  isumshft  12050  geosergap  12066  efsub  12241  sincossq  12308  efieq1re  12332  bezoutlema  12569  bezoutlemb  12570  eucalg  12630  phiprmpw  12793  modprmn0modprm0  12828  coprimeprodsq  12829  pythagtriplem15  12850  pythagtriplem17  12852  fldivp1  12920  1arithlem4  12938  strsetsid  13114  setsslid  13132  pwsbas  13374  opprunitd  14123  cnfldsub  14588  upxp  14995  uptx  14997  perfectlem2  15723  lgsdilem  15755  gausslemma2dlem1a  15786  2sqlem3  15845