Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3eqtrrd GIF version

Theorem 3eqtrrd 2177
 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
StepHypRef Expression
1 3eqtrd.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2eqtrd 2172 . 2 (𝜑𝐴 = 𝐶)
4 3eqtrd.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2173 1 (𝜑𝐷 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132 This theorem is referenced by:  nnanq0  7278  1idprl  7410  1idpru  7411  axcnre  7701  fseq1p1m1  9886  expmulzap  10351  expubnd  10362  subsq  10411  bcm1k  10518  bcpasc  10524  crim  10642  rereb  10647  fsumparts  11251  isumshft  11271  geosergap  11287  efsub  11399  sincossq  11466  efieq1re  11489  bezoutlema  11698  bezoutlemb  11699  eucalg  11751  phiprmpw  11909  strsetsid  12006  setsslid  12023  upxp  12455  uptx  12457
 Copyright terms: Public domain W3C validator