Theorem 3eqtrrd 2231

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 2226	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2227	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  nnanq0  7520  1idprl  7652  1idpru  7653  axcnre  7943  fseq1p1m1  10163  seqf1oglem1  10593  expmulzap  10659  expubnd  10670  subsq  10720  bcm1k  10834  bcpasc  10840  crim  11005  rereb  11010  fsumparts  11616  isumshft  11636  geosergap  11652  efsub  11827  sincossq  11894  efieq1re  11918  bezoutlema  12139  bezoutlemb  12140  eucalg  12200  phiprmpw  12363  modprmn0modprm0  12397  coprimeprodsq  12398  pythagtriplem15  12419  pythagtriplem17  12421  fldivp1  12489  1arithlem4  12507  strsetsid  12654  setsslid  12672  opprunitd  13609  cnfldsub  14074  upxp  14451  uptx  14453  lgsdilem  15184  gausslemma2dlem1a  15215  2sqlem3  15274