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

Theorem neli 3049
Description: Inference associated with df-nel 3048. (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 3048 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 229 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2104  wnel 3047
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 206  df-nel 3048
This theorem is referenced by:  alephprc  9905  pnfnre2  11067  renepnf  11073  renemnf  11074  ltxrlt  11095  nn0nepnf  12363  xrltnr  12905  pnfnlt  12914  nltmnf  12915  hashclb  14122  hasheq0  14127  egt2lt3  15964  nthruc  16010  pcgcd1  16627  pc2dvds  16629  ramtcl2  16761  nsmndex1  18601  odhash3  19230  xrsmgmdifsgrp  20684  xrsdsreclblem  20693  topnex  22195  pnfnei  22420  mnfnei  22421  zclmncvs  24361  i1f0rn  24895  deg1nn0clb  25304  rgrx0ndm  28009  rgrx0nd  28010  f1resfz0f1d  33121  gonan0  33403  inaex  42128  mnfnre2  43164
  Copyright terms: Public domain W3C validator