Theorem 3eqtrrd 2276

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  nnanq0  7826  1idprl  7958  1idpru  7959  axcnre  8249  fseq1p1m1  10512  seqf1oglem1  10971  expmulzap  11037  expubnd  11048  subsq  11098  bcm1k  11214  bcpasc  11220  crim  11639  rereb  11644  fsumparts  12256  isumshft  12276  geosergap  12292  efsub  12467  sincossq  12534  efieq1re  12558  bezoutlema  12795  bezoutlemb  12796  eucalg  12856  phiprmpw  13023  modprmn0modprm0  13058  coprimeprodsq  13059  pythagtriplem15  13080  pythagtriplem17  13082  fldivp1  13150  1arithlem4  13168  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemic  13302  ballotfilem1c  13303  strsetsid  13437  setsslid  13455  pwsbas  14289  opprunitd  14501  cnfldsub  14996  upxp  15464  uptx  15466  perfectlem2  16261  lgsdilem  16312  gausslemma2dlem1a  16343  2sqlem3  16402