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

Theorem syl6eqel 2125
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eqel.1 (φA = B)
syl6eqel.2 B 𝐶
Assertion
Ref Expression
syl6eqel (φA 𝐶)

Proof of Theorem syl6eqel
StepHypRef Expression
1 syl6eqel.1 . 2 (φA = B)
2 syl6eqel.2 . . 3 B 𝐶
32a1i 9 . 2 (φB 𝐶)
41, 3eqeltrd 2111 1 (φA 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242   wcel 1390
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033
This theorem is referenced by:  syl6eqelr  2126  snexprc  3929  onsucelsucexmidlem  4214  ovprc  5482  nnmcl  5999  xpsnen  6231  indpi  6326  nq0m0r  6439  genpelxp  6494  un0mulcl  7992  znegcl  8052  zeo  8119  eqreznegel  8325  xnegcl  8515  expival  8911  expcllem  8920  m1expcl2  8931
  Copyright terms: Public domain W3C validator