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

Theorem syl5eqel 2106
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eqel.1 A = B
syl5eqel.2 (φB 𝐶)
Assertion
Ref Expression
syl5eqel (φA 𝐶)

Proof of Theorem syl5eqel
StepHypRef Expression
1 syl5eqel.1 . . 3 A = B
21a1i 9 . 2 (φA = B)
3 syl5eqel.2 . 2 (φB 𝐶)
42, 3eqeltrd 2096 1 (φA 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228   wcel 1374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-clel 2018
This theorem is referenced by:  syl5eqelr  2107  csbexgOLD  3859  otexg  3941  tpexg  4129  dmresexg  4561  f1oabexg  5063  funfvex  5117  riotaprop  5415  fnovex  5462  fovrn  5566  fnovrn  5571  cofunexg  5661  cofunex2g  5662  abrexex2g  5670  xpexgALT  5683  mpt2fvex  5752  tfrex  5876  rdgi0g  5886  ecexg  6021  qsexg  6073  negcl  6798  bj-snexg  7135
  Copyright terms: Public domain W3C validator