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

Theorem syl6eleqr 2181
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 2092 . 2  |-  B  =  C
41, 3syl6eleq 2180 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289    e. wcel 1438
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  brelrng  4654  elabrex  5519  fliftel1  5555  ovidig  5744  unielxp  5926  2oconcl  6185  ecopqsi  6327  eroprf  6365  sbthlem2  6646  djulclr  6720  djurclr  6721  djulcl  6722  djurcl  6723  isnumi  6789  addclnq  6913  mulclnq  6914  recexnq  6928  ltexnqq  6946  prarloclemarch  6956  prarloclemarch2  6957  nnnq  6960  nqnq0  6979  addclnq0  6989  mulclnq0  6990  nqpnq0nq  6991  prarloclemlt  7031  prarloclemlo  7032  prarloclemcalc  7040  nqprm  7080  cauappcvgprlem2  7198  caucvgprlem2  7218  addclsr  7278  mulclsr  7279  prsrcl  7308  pitonnlem2  7363  pitore  7366  recnnre  7367  axaddcl  7380  axmulcl  7382  axcaucvglemcl  7409  axcaucvglemval  7411  axcaucvglemcau  7412  axcaucvglemres  7413  uztrn2  9005  eluz2nn  9026  peano2uzs  9041  rebtwn2z  9631  iseqfcl  9843  iseqfclt  9844  seqf  9845  iser0  9912  ser0  9914  bcm1k  10133  bcp1nk  10135  bcpasc  10139  hashennn  10153  hashcl  10154  climconst  10642  climshft2  10659  clim2ser  10689  clim2ser2  10690  iserex  10691  serif0  10705  zisum  10738  fsump1i  10790  isumshft  10846  isumsplit  10847  isum1p  10848  isumrpcl  10850  cvgratnnlemseq  10881  cvgratz  10887  cvgratgt0  10888  dvdsflip  10945  fzo0dvdseq  10951  gcdsupcl  11043  ialgr0  11119  prmind2  11195  crth  11293  djulclALT  11358  djurclALT  11359
  Copyright terms: Public domain W3C validator