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

Theorem syl6eqel 2206
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 2192 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  wcel 1463
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111
This theorem is referenced by:  syl6eqelr  2207  snexprc  4078  onsucelsucexmidlem  4412  dcextest  4463  nnpredcl  4504  ovprc  5772  nnmcl  6343  xpsnen  6681  xpfi  6784  snexxph  6804  ctssdclemn0  6961  indpi  7114  nq0m0r  7228  genpelxp  7283  un0mulcl  8962  znegcl  9036  zeo  9107  eqreznegel  9355  xnegcl  9555  modqid0  10063  q2txmodxeq0  10097  ser0  10227  expcllem  10244  m1expcl2  10255  bcval  10435  bccl  10453  hashinfom  10464  resqrexlemlo  10725  iserge0  11052  sumrbdclem  11085  fsum3cvg  11086  summodclem3  11089  summodclem2a  11090  fisumss  11101  binom  11193  bcxmas  11198  gcdval  11544  gcdcl  11551  lcmcl  11649  ssblps  12489  ssbl  12490  xmeter  12500  blssioo  12609  nninfsellemeqinf  13023  nninffeq  13027  isomninnlem  13036  trilpolemclim  13040
  Copyright terms: Public domain W3C validator