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

Theorem syl5req 2161
 Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl5req.1 𝐴 = 𝐵
syl5req.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
syl5req (𝜑𝐶 = 𝐴)

Proof of Theorem syl5req
StepHypRef Expression
1 syl5req.1 . . 3 𝐴 = 𝐵
2 syl5req.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2syl5eq 2160 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2121 1 (𝜑𝐶 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1314 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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-cleq 2108 This theorem is referenced by:  syl5reqr  2163  opeqsn  4142  dcextest  4463  relop  4657  funopg  5125  funcnvres  5164  mapsnconst  6554  snexxph  6804  apreap  8312  recextlem1  8372  nn0supp  8980  intqfrac2  10032  hashprg  10494  hashfacen  10519  explecnv  11214  rerestcntop  12614
 Copyright terms: Public domain W3C validator