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

Theorem syl6eleqr 2209
Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
syl6eleqr.1  |-  ( ph  ->  A  e.  B )
syl6eleqr.2  |-  C  =  B
Assertion
Ref Expression
syl6eleqr  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl6eleqr
StepHypRef Expression
1 syl6eleqr.1 . 2  |-  ( ph  ->  A  e.  B )
2 syl6eleqr.2 . . 3  |-  C  =  B
32eqcomi 2119 . 2  |-  B  =  C
41, 3syl6eleq 2208 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:  brelrng  4738  elabrex  5625  fliftel1  5661  ovidig  5854  unielxp  6038  2oconcl  6302  ecopqsi  6450  eroprf  6488  sbthlem2  6812  djulclr  6900  djurclr  6901  djulcl  6902  djurcl  6903  caseinl  6942  caseinr  6943  ctssdccl  6962  isnumi  7004  addclnq  7147  mulclnq  7148  recexnq  7162  ltexnqq  7180  prarloclemarch  7190  prarloclemarch2  7191  nnnq  7194  nqnq0  7213  addclnq0  7223  mulclnq0  7224  nqpnq0nq  7225  prarloclemlt  7265  prarloclemlo  7266  prarloclemcalc  7274  nqprm  7314  cauappcvgprlem2  7432  caucvgprlem2  7452  addclsr  7525  mulclsr  7526  prsrcl  7556  mappsrprg  7576  suplocsrlemb  7578  pitonnlem2  7619  pitore  7622  recnnre  7623  axaddcl  7636  axmulcl  7638  axcaucvglemcl  7667  axcaucvglemval  7669  axcaucvglemcau  7670  axcaucvglemres  7671  uztrn2  9295  eluz2nn  9316  peano2uzs  9331  rebtwn2z  9983  seqf  10185  ser0  10238  bcm1k  10457  bcp1nk  10459  bcpasc  10463  hashennn  10477  hashcl  10478  climconst  11010  climshft2  11026  clim2ser  11057  clim2ser2  11058  iserex  11059  serf0  11072  zsumdc  11104  fsump1i  11153  iserabs  11195  isumshft  11210  isumsplit  11211  isum1p  11212  isumrpcl  11214  cvgratnnlemseq  11246  cvgratz  11252  cvgratgt0  11253  ef0lem  11276  dvdsflip  11456  fzo0dvdseq  11462  gcdsupcl  11554  ialgr0  11632  prmind2  11708  crth  11806  ennnfonelemkh  11831  ennnfonelemrn  11838  ennnfonelemdm  11839  ctiunctlemf  11857  strslfv2d  11907  1strbas  11964  2strbasg  11966  2stropg  11967  2strbas1g  11969  rngbaseg  11981  rngplusgg  11982  rngmulrg  11983  srngbased  11988  srngplusgd  11989  srngmulrd  11990  srnginvld  11991  lmodbased  11999  lmodplusgd  12000  lmodscad  12001  lmodvscad  12002  ipsbased  12007  ipsaddgd  12008  ipsmulrd  12009  ipsscad  12010  ipsvscad  12011  ipsipd  12012  topgrpbasd  12017  topgrpplusgd  12018  topgrptsetd  12019  lmconst  12291  lmss  12321  uptx  12349  cnmpt1res  12371  dvidlemap  12735  dvrecap  12752  djulclALT  12842  djurclALT  12843  pwle2  13027  trilpolemeq1  13067
  Copyright terms: Public domain W3C validator