Theorem 3eqtrrd 2267

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  nnanq0  7668  1idprl  7800  1idpru  7801  axcnre  8091  fseq1p1m1  10319  seqf1oglem1  10771  expmulzap  10837  expubnd  10848  subsq  10898  bcm1k  11012  bcpasc  11018  crim  11409  rereb  11414  fsumparts  12021  isumshft  12041  geosergap  12057  efsub  12232  sincossq  12299  efieq1re  12323  bezoutlema  12560  bezoutlemb  12561  eucalg  12621  phiprmpw  12784  modprmn0modprm0  12819  coprimeprodsq  12820  pythagtriplem15  12841  pythagtriplem17  12843  fldivp1  12911  1arithlem4  12929  strsetsid  13105  setsslid  13123  pwsbas  13365  opprunitd  14114  cnfldsub  14579  upxp  14986  uptx  14988  perfectlem2  15714  lgsdilem  15746  gausslemma2dlem1a  15777  2sqlem3  15836