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

Theorem syl6eqel 2208
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 2194 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  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  8979  znegcl  9053  zeo  9124  eqreznegel  9374  xnegcl  9583  modqid0  10091  q2txmodxeq0  10125  ser0  10255  expcllem  10272  m1expcl2  10283  bcval  10463  bccl  10481  hashinfom  10492  resqrexlemlo  10753  iserge0  11080  sumrbdclem  11113  fsum3cvg  11114  summodclem3  11117  summodclem2a  11118  fisumss  11129  binom  11221  bcxmas  11226  gcdval  11575  gcdcl  11582  lcmcl  11680  ssblps  12521  ssbl  12522  xmeter  12532  blssioo  12641  nninfsellemeqinf  13139  nninffeq  13143  isomninnlem  13152  trilpolemclim  13156
  Copyright terms: Public domain W3C validator