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 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  nnanq0  7815  1idprl  7947  1idpru  7948  axcnre  8238  fseq1p1m1  10479  seqf1oglem1  10934  expmulzap  11000  expubnd  11011  subsq  11061  bcm1k  11176  bcpasc  11182  crim  11601  rereb  11606  fsumparts  12215  isumshft  12235  geosergap  12251  efsub  12426  sincossq  12493  efieq1re  12517  bezoutlema  12754  bezoutlemb  12755  eucalg  12815  phiprmpw  12978  modprmn0modprm0  13013  coprimeprodsq  13014  pythagtriplem15  13035  pythagtriplem17  13037  fldivp1  13105  1arithlem4  13123  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemic  13228  ballotfilem1c  13229  strsetsid  13363  setsslid  13381  pwsbas  14182  opprunitd  14390  cnfldsub  14884  upxp  15296  uptx  15298  perfectlem2  16028  lgsdilem  16060  gausslemma2dlem1a  16091  2sqlem3  16150