Theorem 3eqtrrd 2215

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  nnanq0  7459  1idprl  7591  1idpru  7592  axcnre  7882  fseq1p1m1  10096  expmulzap  10568  expubnd  10579  subsq  10629  bcm1k  10742  bcpasc  10748  crim  10869  rereb  10874  fsumparts  11480  isumshft  11500  geosergap  11516  efsub  11691  sincossq  11758  efieq1re  11781  bezoutlema  12002  bezoutlemb  12003  eucalg  12061  phiprmpw  12224  modprmn0modprm0  12258  coprimeprodsq  12259  pythagtriplem15  12280  pythagtriplem17  12282  fldivp1  12348  1arithlem4  12366  strsetsid  12497  setsslid  12515  opprunitd  13284  cnfldsub  13554  upxp  13857  uptx  13859  lgsdilem  14513  2sqlem3  14549