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

Theorem syl6eleq 2208
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eleq.1  |-  ( ph  ->  A  e.  B )
syl6eleq.2  |-  B  =  C
Assertion
Ref Expression
syl6eleq  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl6eleq
StepHypRef Expression
1 syl6eleq.1 . 2  |-  ( ph  ->  A  e.  B )
2 syl6eleq.2 . . 3  |-  B  =  C
32a1i 9 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2194 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314    e. wcel 1463
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-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  syl6eleqr  2209  prid2g  3596  freccllem  6265  finomni  6978  exmidomniim  6979  ismkvnex  6995  exmidaclem  7028  caucvgprprlem2  7482  gt0srpr  7520  eluzel2  9283  fseq1p1m1  9825  fznn0sub2  9856  nn0split  9864  nnsplit  9865  exple1  10300  bcval5  10460  bcpasc  10463  zfz1isolemsplit  10532  seq3coll  10536  clim2ser  11057  clim2ser2  11058  iserex  11059  isermulc2  11060  iserle  11062  iserge0  11063  climub  11064  climserle  11065  serf0  11072  summodclem3  11100  summodclem2a  11101  fsum3  11107  sum0  11108  fsumcl2lem  11118  fsumadd  11126  isumclim3  11143  isumadd  11151  fsump1i  11153  fsummulc2  11168  cvgcmpub  11196  binom1dif  11207  isumshft  11210  isumsplit  11211  isumrpcl  11214  arisum2  11219  trireciplem  11220  geoserap  11227  geolim  11231  geo2lim  11236  cvgratnnlemnexp  11244  cvgratnnlemseq  11246  cvgratgt0  11253  mertenslemi1  11255  mertenslem2  11256  mertensabs  11257  efcvgfsum  11283  efcj  11289  effsumlt  11308  mod2eq1n2dvds  11483  algrp1  11634  phiprmpw  11804  crth  11806  phimullem  11807  ennnfonelemp1  11825  istps  12105  topontopn  12110  cldrcl  12177  cnrehmeocntop  12668  nnsf  13033  nninfsellemqall  13045  nninfomnilem  13048  cvgcmp2nlemabs  13061  trilpolemeq1  13067
  Copyright terms: Public domain W3C validator