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

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

Proof of Theorem syl5eqel
StepHypRef Expression
1 syl5eqel.1 . . 3 𝐴 = 𝐵
21a1i 9 . 2 (𝜑𝐴 = 𝐵)
3 syl5eqel.2 . 2 (𝜑𝐵𝐶)
42, 3eqeltrd 2130 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  syl5eqelr  2141  csbexga  3913  otexg  3995  tpexg  4207  dmresexg  4662  f1oabexg  5166  funfvex  5220  riotaexg  5500  riotaprop  5519  fnovex  5566  ovexg  5567  fovrn  5671  fnovrn  5676  cofunexg  5766  cofunex2g  5767  abrexex2g  5775  xpexgALT  5788  mpt2fvex  5857  tfrex  5985  frec0g  6014  ecexg  6141  qsexg  6193  diffifi  6382  addvalex  6978  negcl  7274  intqfrac2  9269  intfracq  9270  frecuzrdgrrn  9358  ibcval5  9631  climmpt  10052  ialgcvg  10270  ialgcvga  10273  ialgfx  10274  bj-snexg  10419
  Copyright terms: Public domain W3C validator