Theorem 3eqtrrd 2267

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  nnanq0  7641  1idprl  7773  1idpru  7774  axcnre  8064  fseq1p1m1  10286  seqf1oglem1  10736  expmulzap  10802  expubnd  10813  subsq  10863  bcm1k  10977  bcpasc  10983  crim  11364  rereb  11369  fsumparts  11976  isumshft  11996  geosergap  12012  efsub  12187  sincossq  12254  efieq1re  12278  bezoutlema  12515  bezoutlemb  12516  eucalg  12576  phiprmpw  12739  modprmn0modprm0  12774  coprimeprodsq  12775  pythagtriplem15  12796  pythagtriplem17  12798  fldivp1  12866  1arithlem4  12884  strsetsid  13060  setsslid  13078  pwsbas  13320  opprunitd  14068  cnfldsub  14533  upxp  14940  uptx  14942  perfectlem2  15668  lgsdilem  15700  gausslemma2dlem1a  15731  2sqlem3  15790