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

Theorem syl6eqel 2144
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 2130 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259    e. wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  syl6eqelr  2145  snexprc  3966  onsucelsucexmidlem  4282  ovprc  5568  nnmcl  6091  xpsnen  6326  indpi  6498  nq0m0r  6612  genpelxp  6667  un0mulcl  8273  znegcl  8333  zeo  8402  eqreznegel  8646  xnegcl  8846  modqid0  9300  q2txmodxeq0  9334  iser0  9415  expival  9422  expcllem  9431  m1expcl2  9442  bcval  9617  bccl  9635  resqrexlemlo  9840  iserige0  10094
  Copyright terms: Public domain W3C validator