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  10517  seqf1oglem1  10976  expmulzap  11042  expubnd  11053  subsq  11103  bcm1k  11219  bcpasc  11225  crim  11644  rereb  11649  fsumparts  12261  isumshft  12281  geosergap  12297  efsub  12472  sincossq  12539  efieq1re  12563  bezoutlema  12800  bezoutlemb  12801  eucalg  12861  phiprmpw  13028  modprmn0modprm0  13063  coprimeprodsq  13064  pythagtriplem15  13085  pythagtriplem17  13087  fldivp1  13155  1arithlem4  13173  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemic  13307  ballotfilem1c  13308  strsetsid  13442  setsslid  13460  pwsbas  14311  opprunitd  14525  cnfldsub  15020  upxp  15515  uptx  15517  perfectlem2  16317  lgsdilem  16368  gausslemma2dlem1a  16399  2sqlem3  16458