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

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

Proof of Theorem syl6eqel
StepHypRef Expression
1 syl6eqel.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eqel.2 . . 3 𝐵𝐶
32a1i 9 . 2 (𝜑𝐵𝐶)
41, 3eqeltrd 2130 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  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  3965  onsucelsucexmidlem  4281  ovprc  5567  nnmcl  6090  xpsnen  6325  indpi  6497  nq0m0r  6611  genpelxp  6666  un0mulcl  8272  znegcl  8332  zeo  8401  eqreznegel  8645  xnegcl  8845  modqid0  9299  q2txmodxeq0  9333  iser0  9414  expival  9421  expcllem  9430  m1expcl2  9441  bcval  9616  bccl  9634  resqrexlemlo  9839  iserige0  10093
  Copyright terms: Public domain W3C validator