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

Theorem syl5eqel 2171
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 2161 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  syl5eqelr  2172  csbexga  3944  otexg  4033  tpexg  4245  dmresexg  4705  f1oabexg  5230  funfvex  5287  riotaexg  5575  riotaprop  5594  fnovex  5641  ovexg  5642  fovrn  5746  fnovrn  5751  cofunexg  5841  cofunex2g  5842  abrexex2g  5850  xpexgALT  5863  mpt2fvex  5932  tfrex  6089  frec0g  6118  freccllem  6123  ecexg  6250  qsexg  6302  pmex  6364  diffifi  6564  unfidisj  6586  prfidisj  6591  tpfidisj  6592  ssfirab  6596  ssfidc  6597  fnfi  6599  funrnfi  6604  infclti  6665  djuex  6683  addvalex  7328  negcl  7629  intqfrac2  9657  intfracq  9658  frec2uzzd  9738  frecuzrdgrrn  9746  iseqf1olemqpcl  9833  iseqf1olemqsum  9837  ibcval5  10071  climmpt  10586  zisum  10668  fsumzcl2  10687  ialgcvg  10936  ialgcvga  10939  ialgfx  10940  eucialgcvga  10946  eucialg  10947  crth  11106  phimullem  11107  bj-snexg  11272
  Copyright terms: Public domain W3C validator