Theorem 3eqtrrd 2234

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  nnanq0  7544  1idprl  7676  1idpru  7677  axcnre  7967  fseq1p1m1  10188  seqf1oglem1  10630  expmulzap  10696  expubnd  10707  subsq  10757  bcm1k  10871  bcpasc  10877  crim  11042  rereb  11047  fsumparts  11654  isumshft  11674  geosergap  11690  efsub  11865  sincossq  11932  efieq1re  11956  bezoutlema  12193  bezoutlemb  12194  eucalg  12254  phiprmpw  12417  modprmn0modprm0  12452  coprimeprodsq  12453  pythagtriplem15  12474  pythagtriplem17  12476  fldivp1  12544  1arithlem4  12562  strsetsid  12738  setsslid  12756  pwsbas  12996  opprunitd  13744  cnfldsub  14209  upxp  14616  uptx  14618  perfectlem2  15344  lgsdilem  15376  gausslemma2dlem1a  15407  2sqlem3  15466