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  7542  1idprl  7674  1idpru  7675  axcnre  7965  fseq1p1m1  10186  seqf1oglem1  10628  expmulzap  10694  expubnd  10705  subsq  10755  bcm1k  10869  bcpasc  10875  crim  11040  rereb  11045  fsumparts  11652  isumshft  11672  geosergap  11688  efsub  11863  sincossq  11930  efieq1re  11954  bezoutlema  12191  bezoutlemb  12192  eucalg  12252  phiprmpw  12415  modprmn0modprm0  12450  coprimeprodsq  12451  pythagtriplem15  12472  pythagtriplem17  12474  fldivp1  12542  1arithlem4  12560  strsetsid  12736  setsslid  12754  pwsbas  12994  opprunitd  13742  cnfldsub  14207  upxp  14592  uptx  14594  perfectlem2  15320  lgsdilem  15352  gausslemma2dlem1a  15383  2sqlem3  15442