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

Theorem syl6eleqr 2131
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 2044 . 2  |-  B  =  C
41, 3syl6eleq 2130 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243    e. wcel 1393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036
This theorem is referenced by:  brelrng  4565  elabrex  5397  fliftel1  5434  ovidig  5618  unielxp  5800  2oconcl  6022  ecopqsi  6161  eroprf  6199  isnumi  6362  addclnq  6473  mulclnq  6474  recexnq  6488  ltexnqq  6506  prarloclemarch  6516  prarloclemarch2  6517  nnnq  6520  nqnq0  6539  addclnq0  6549  mulclnq0  6550  nqpnq0nq  6551  prarloclemlt  6591  prarloclemlo  6592  prarloclemcalc  6600  nqprm  6640  cauappcvgprlem2  6758  caucvgprlem2  6778  addclsr  6838  mulclsr  6839  prsrcl  6868  pitonnlem2  6923  pitore  6926  recnnre  6927  axaddcl  6940  axmulcl  6942  axcaucvglemcl  6969  axcaucvglemval  6971  axcaucvglemcau  6972  axcaucvglemres  6973  uztrn2  8490  eluz2nn  8511  peano2uzs  8527  rebtwn2z  9109  iser0  9250  climconst  9811  climshft2  9827  clim2iser  9857  clim2iser2  9858  iiserex  9859  serif0  9871  ialgr0  9883
  Copyright terms: Public domain W3C validator