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

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

Proof of Theorem syl6eqel
StepHypRef Expression
1 syl6eqel.1 . 2  |-  ( ph  ->  A  =  B )
2 syl6eqel.2 . . 3  |-  B  e.  C
32a1i 9 . 2  |-  ( ph  ->  B  e.  C )
41, 3eqeltrd 2194 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    e. wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  syl6eqelr  2209  snexprc  4080  onsucelsucexmidlem  4414  dcextest  4465  nnpredcl  4506  ovprc  5774  nnmcl  6345  xpsnen  6683  xpfi  6786  snexxph  6806  ctssdclemn0  6963  exmidonfinlem  7017  indpi  7118  nq0m0r  7232  genpelxp  7287  un0mulcl  8969  znegcl  9043  zeo  9114  eqreznegel  9362  xnegcl  9570  modqid0  10078  q2txmodxeq0  10112  ser0  10242  expcllem  10259  m1expcl2  10270  bcval  10450  bccl  10468  hashinfom  10479  resqrexlemlo  10740  iserge0  11067  sumrbdclem  11100  fsum3cvg  11101  summodclem3  11104  summodclem2a  11105  fisumss  11116  binom  11208  bcxmas  11213  gcdval  11560  gcdcl  11567  lcmcl  11665  ssblps  12505  ssbl  12506  xmeter  12516  blssioo  12625  nninfsellemeqinf  13108  nninffeq  13112  isomninnlem  13121  trilpolemclim  13125
  Copyright terms: Public domain W3C validator