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

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

Proof of Theorem eleqtrrdi
StepHypRef Expression
1 eleqtrrdi.1 . 2  |-  ( ph  ->  A  e.  B )
2 eleqtrrdi.2 . . 3  |-  C  =  B
32eqcomi 2143 . 2  |-  B  =  C
41, 3eleqtrdi 2232 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331    e. wcel 1480
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  brelrng  4770  elabrex  5659  fliftel1  5695  ovidig  5888  unielxp  6072  2oconcl  6336  ecopqsi  6484  eroprf  6522  sbthlem2  6846  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  caseinl  6976  caseinr  6977  ctssdccl  6996  isnumi  7043  addclnq  7195  mulclnq  7196  recexnq  7210  ltexnqq  7228  prarloclemarch  7238  prarloclemarch2  7239  nnnq  7242  nqnq0  7261  addclnq0  7271  mulclnq0  7272  nqpnq0nq  7273  prarloclemlt  7313  prarloclemlo  7314  prarloclemcalc  7322  nqprm  7362  cauappcvgprlem2  7480  caucvgprlem2  7500  addclsr  7573  mulclsr  7574  prsrcl  7604  mappsrprg  7624  suplocsrlemb  7626  pitonnlem2  7667  pitore  7670  recnnre  7671  axaddcl  7684  axmulcl  7686  axcaucvglemcl  7715  axcaucvglemval  7717  axcaucvglemcau  7718  axcaucvglemres  7719  uztrn2  9355  eluz2nn  9376  peano2uzs  9391  rebtwn2z  10044  seqf  10246  ser0  10299  bcm1k  10518  bcp1nk  10520  bcpasc  10524  hashennn  10538  hashcl  10539  climconst  11071  climshft2  11087  clim2ser  11118  clim2ser2  11119  iserex  11120  serf0  11133  zsumdc  11165  fsump1i  11214  iserabs  11256  isumshft  11271  isumsplit  11272  isum1p  11273  isumrpcl  11275  cvgratnnlemseq  11307  cvgratz  11313  cvgratgt0  11314  clim2prod  11320  clim2divap  11321  prodf1  11323  ntrivcvgap0  11330  ef0lem  11378  dvdsflip  11560  fzo0dvdseq  11566  gcdsupcl  11658  ialgr0  11736  prmind2  11812  crth  11911  ennnfonelemkh  11936  ennnfonelemrn  11943  ennnfonelemdm  11944  ctiunctlemf  11962  strslfv2d  12015  1strbas  12072  2strbasg  12074  2stropg  12075  2strbas1g  12077  rngbaseg  12089  rngplusgg  12090  rngmulrg  12091  srngbased  12096  srngplusgd  12097  srngmulrd  12098  srnginvld  12099  lmodbased  12107  lmodplusgd  12108  lmodscad  12109  lmodvscad  12110  ipsbased  12115  ipsaddgd  12116  ipsmulrd  12117  ipsscad  12118  ipsvscad  12119  ipsipd  12120  topgrpbasd  12125  topgrpplusgd  12126  topgrptsetd  12127  lmconst  12399  lmss  12429  uptx  12457  cnmpt1res  12479  dvidlemap  12843  dvrecap  12860  pilem3  12886  djulclALT  13113  djurclALT  13114  pwle2  13298  trilpolemeq1  13340
  Copyright terms: Public domain W3C validator