Theorem 3eqtrrd 2245

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  nnanq0  7606  1idprl  7738  1idpru  7739  axcnre  8029  fseq1p1m1  10251  seqf1oglem1  10701  expmulzap  10767  expubnd  10778  subsq  10828  bcm1k  10942  bcpasc  10948  crim  11284  rereb  11289  fsumparts  11896  isumshft  11916  geosergap  11932  efsub  12107  sincossq  12174  efieq1re  12198  bezoutlema  12435  bezoutlemb  12436  eucalg  12496  phiprmpw  12659  modprmn0modprm0  12694  coprimeprodsq  12695  pythagtriplem15  12716  pythagtriplem17  12718  fldivp1  12786  1arithlem4  12804  strsetsid  12980  setsslid  12998  pwsbas  13239  opprunitd  13987  cnfldsub  14452  upxp  14859  uptx  14861  perfectlem2  15587  lgsdilem  15619  gausslemma2dlem1a  15650  2sqlem3  15709