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  7825  1idprl  7957  1idpru  7958  axcnre  8248  fseq1p1m1  10511  seqf1oglem1  10969  expmulzap  11035  expubnd  11046  subsq  11096  bcm1k  11212  bcpasc  11218  crim  11637  rereb  11642  fsumparts  12253  isumshft  12273  geosergap  12289  efsub  12464  sincossq  12531  efieq1re  12555  bezoutlema  12792  bezoutlemb  12793  eucalg  12853  phiprmpw  13020  modprmn0modprm0  13055  coprimeprodsq  13056  pythagtriplem15  13077  pythagtriplem17  13079  fldivp1  13147  1arithlem4  13165  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemic  13299  ballotfilem1c  13300  strsetsid  13434  setsslid  13452  pwsbas  14254  opprunitd  14466  cnfldsub  14961  upxp  15422  uptx  15424  perfectlem2  16198  lgsdilem  16244  gausslemma2dlem1a  16275  2sqlem3  16334