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  7518  1idprl  7650  1idpru  7651  axcnre  7941  fseq1p1m1  10160  seqf1oglem1  10590  expmulzap  10656  expubnd  10667  subsq  10717  bcm1k  10831  bcpasc  10837  crim  11002  rereb  11007  fsumparts  11613  isumshft  11633  geosergap  11649  efsub  11824  sincossq  11891  efieq1re  11915  bezoutlema  12136  bezoutlemb  12137  eucalg  12197  phiprmpw  12360  modprmn0modprm0  12394  coprimeprodsq  12395  pythagtriplem15  12416  pythagtriplem17  12418  fldivp1  12486  1arithlem4  12504  strsetsid  12651  setsslid  12669  opprunitd  13606  cnfldsub  14063  upxp  14440  uptx  14442  lgsdilem  15143  gausslemma2dlem1a  15174  2sqlem3  15204