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  7525  1idprl  7657  1idpru  7658  axcnre  7948  fseq1p1m1  10169  seqf1oglem1  10611  expmulzap  10677  expubnd  10688  subsq  10738  bcm1k  10852  bcpasc  10858  crim  11023  rereb  11028  fsumparts  11635  isumshft  11655  geosergap  11671  efsub  11846  sincossq  11913  efieq1re  11937  bezoutlema  12166  bezoutlemb  12167  eucalg  12227  phiprmpw  12390  modprmn0modprm0  12425  coprimeprodsq  12426  pythagtriplem15  12447  pythagtriplem17  12449  fldivp1  12517  1arithlem4  12535  strsetsid  12711  setsslid  12729  opprunitd  13666  cnfldsub  14131  upxp  14508  uptx  14510  perfectlem2  15236  lgsdilem  15268  gausslemma2dlem1a  15299  2sqlem3  15358