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

Theorem syl5eqelr 2182
 Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eqelr.1 𝐵 = 𝐴
syl5eqelr.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
syl5eqelr (𝜑𝐴𝐶)

Proof of Theorem syl5eqelr
StepHypRef Expression
1 syl5eqelr.1 . . 3 𝐵 = 𝐴
21eqcomi 2099 . 2 𝐴 = 𝐵
3 syl5eqelr.2 . 2 (𝜑𝐵𝐶)
42, 3syl5eqel 2181 1 (𝜑𝐴𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1296   ∈ wcel 1445 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077 This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091 This theorem is referenced by:  dmrnssfld  4728  cnvexg  5002  opabbrex  5731  offval  5901  resfunexgALT  5919  abrexexg  5927  abrexex2g  5929  opabex3d  5930  unfidisj  6712  nqprlu  7203  iccshftr  9560  iccshftl  9562  iccdil  9564  icccntr  9566  mertenslem2  11079  exprmfct  11546  0opn  11857  difopn  11960  tgrest  12021  cnmptid  12103  cnmptc  12104
 Copyright terms: Public domain W3C validator