Theorem 3eqtrrd 2272

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  nnanq0  7775  1idprl  7907  1idpru  7908  axcnre  8198  fseq1p1m1  10432  seqf1oglem1  10885  expmulzap  10951  expubnd  10962  subsq  11012  bcm1k  11126  bcpasc  11132  crim  11547  rereb  11552  fsumparts  12160  isumshft  12180  geosergap  12196  efsub  12371  sincossq  12438  efieq1re  12462  bezoutlema  12699  bezoutlemb  12700  eucalg  12760  phiprmpw  12923  modprmn0modprm0  12958  coprimeprodsq  12959  pythagtriplem15  12980  pythagtriplem17  12982  fldivp1  13050  1arithlem4  13068  strsetsid  13262  setsslid  13280  pwsbas  13522  opprunitd  14272  cnfldsub  14740  upxp  15154  uptx  15156  perfectlem2  15885  lgsdilem  15917  gausslemma2dlem1a  15948  2sqlem3  16007