Theorem 3eqtrrd 2225

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

Syntax hints:   → wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169

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

This theorem is referenced by:  nnanq0  7471  1idprl  7603  1idpru  7604  axcnre  7894  fseq1p1m1  10108  expmulzap  10580  expubnd  10591  subsq  10641  bcm1k  10754  bcpasc  10760  crim  10881  rereb  10886  fsumparts  11492  isumshft  11512  geosergap  11528  efsub  11703  sincossq  11770  efieq1re  11793  bezoutlema  12014  bezoutlemb  12015  eucalg  12073  phiprmpw  12236  modprmn0modprm0  12270  coprimeprodsq  12271  pythagtriplem15  12292  pythagtriplem17  12294  fldivp1  12360  1arithlem4  12378  strsetsid  12509  setsslid  12527  opprunitd  13358  cnfldsub  13751  upxp  14068  uptx  14070  lgsdilem  14724  2sqlem3  14760