Theorem 3eqtrrd 2267

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  nnanq0  7656  1idprl  7788  1idpru  7789  axcnre  8079  fseq1p1m1  10302  seqf1oglem1  10753  expmulzap  10819  expubnd  10830  subsq  10880  bcm1k  10994  bcpasc  11000  crim  11384  rereb  11389  fsumparts  11996  isumshft  12016  geosergap  12032  efsub  12207  sincossq  12274  efieq1re  12298  bezoutlema  12535  bezoutlemb  12536  eucalg  12596  phiprmpw  12759  modprmn0modprm0  12794  coprimeprodsq  12795  pythagtriplem15  12816  pythagtriplem17  12818  fldivp1  12886  1arithlem4  12904  strsetsid  13080  setsslid  13098  pwsbas  13340  opprunitd  14089  cnfldsub  14554  upxp  14961  uptx  14963  perfectlem2  15689  lgsdilem  15721  gausslemma2dlem1a  15752  2sqlem3  15811