Theorem 3eqtrrd 2242

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  nnanq0  7570  1idprl  7702  1idpru  7703  axcnre  7993  fseq1p1m1  10215  seqf1oglem1  10662  expmulzap  10728  expubnd  10739  subsq  10789  bcm1k  10903  bcpasc  10909  crim  11140  rereb  11145  fsumparts  11752  isumshft  11772  geosergap  11788  efsub  11963  sincossq  12030  efieq1re  12054  bezoutlema  12291  bezoutlemb  12292  eucalg  12352  phiprmpw  12515  modprmn0modprm0  12550  coprimeprodsq  12551  pythagtriplem15  12572  pythagtriplem17  12574  fldivp1  12642  1arithlem4  12660  strsetsid  12836  setsslid  12854  pwsbas  13095  opprunitd  13843  cnfldsub  14308  upxp  14715  uptx  14717  perfectlem2  15443  lgsdilem  15475  gausslemma2dlem1a  15506  2sqlem3  15565