Theorem 3eqtrrd 2132

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

Syntax hints:   → wi 4   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088

This theorem is referenced by:  nnanq0  7114  1idprl  7246  1idpru  7247  axcnre  7513  fseq1p1m1  9657  expmulzap  10116  expubnd  10127  subsq  10176  bcm1k  10283  bcpasc  10289  crim  10407  rereb  10412  fsumparts  11013  isumshft  11033  geosergap  11049  efsub  11120  sincossq  11188  efieq1re  11210  bezoutlema  11415  bezoutlemb  11416  eucalg  11468  phiprmpw  11625  strsetsid  11676  setsslid  11693