Theorem 3eqtrrd 2243

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

Syntax hints:   → wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  nnanq0  7571  1idprl  7703  1idpru  7704  axcnre  7994  fseq1p1m1  10216  seqf1oglem1  10664  expmulzap  10730  expubnd  10741  subsq  10791  bcm1k  10905  bcpasc  10911  crim  11169  rereb  11174  fsumparts  11781  isumshft  11801  geosergap  11817  efsub  11992  sincossq  12059  efieq1re  12083  bezoutlema  12320  bezoutlemb  12321  eucalg  12381  phiprmpw  12544  modprmn0modprm0  12579  coprimeprodsq  12580  pythagtriplem15  12601  pythagtriplem17  12603  fldivp1  12671  1arithlem4  12689  strsetsid  12865  setsslid  12883  pwsbas  13124  opprunitd  13872  cnfldsub  14337  upxp  14744  uptx  14746  perfectlem2  15472  lgsdilem  15504  gausslemma2dlem1a  15535  2sqlem3  15594