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  7789  1idprl  7921  1idpru  7922  axcnre  8212  fseq1p1m1  10450  seqf1oglem1  10905  expmulzap  10971  expubnd  10982  subsq  11032  bcm1k  11147  bcpasc  11153  crim  11568  rereb  11573  fsumparts  12181  isumshft  12201  geosergap  12217  efsub  12392  sincossq  12459  efieq1re  12483  bezoutlema  12720  bezoutlemb  12721  eucalg  12781  phiprmpw  12944  modprmn0modprm0  12979  coprimeprodsq  12980  pythagtriplem15  13001  pythagtriplem17  13003  fldivp1  13071  1arithlem4  13089  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemic  13194  ballotfilem1c  13195  strsetsid  13329  setsslid  13347  pwsbas  14147  opprunitd  14355  cnfldsub  14849  upxp  15263  uptx  15265  perfectlem2  15994  lgsdilem  16026  gausslemma2dlem1a  16057  2sqlem3  16116