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  7831  1idprl  7963  1idpru  7964  axcnre  8254  fseq1p1m1  10518  seqf1oglem1  10977  expmulzap  11043  expubnd  11054  subsq  11104  bcm1k  11220  bcpasc  11226  crim  11645  rereb  11650  fsumparts  12262  isumshft  12282  geosergap  12298  efsub  12473  sincossq  12540  efieq1re  12564  bezoutlema  12801  bezoutlemb  12802  eucalg  12862  phiprmpw  13029  modprmn0modprm0  13064  coprimeprodsq  13065  pythagtriplem15  13086  pythagtriplem17  13088  fldivp1  13156  1arithlem4  13174  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemic  13308  ballotfilem1c  13309  strsetsid  13443  setsslid  13461  pwsbas  14312  opprunitd  14526  cnfldsub  15021  upxp  15498  uptx  15500  perfectlem2  16300  lgsdilem  16351  gausslemma2dlem1a  16382  2sqlem3  16441