MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neli Unicode version

Theorem neli 2792
Description: Inference associated with df-nel 2655. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
neli.1
Assertion
Ref Expression
neli

Proof of Theorem neli
StepHypRef Expression
1 neli.1 . 2
2 df-nel 2655 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  e.wcel 1818  e/wnel 2653
This theorem is referenced by:  alephprc  8501  renepnf  9662  renemnf  9663  ltxrlt  9676  xrltnr  11359  pnfnlt  11366  nltmnf  11367  hashclb  12430  hasheq0  12433  egt2lt3  13939  nthruc  13984  pcgcd1  14400  pc2dvds  14402  ramtcl2  14529  odhash3  16596  xrsmgmdifsgrp  18455  xrsdsreclblem  18464  pnfnei  19721  mnfnei  19722  i1f0rn  22089  deg1nn0clb  22490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-nel 2655
  Copyright terms: Public domain W3C validator