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

Theorem neli 3038
Description: Inference associated with df-nel 3037. (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 3037 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 220 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2140  wnel 3036
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 197  df-nel 3037
This theorem is referenced by:  alephprc  9133  renepnf  10300  renemnf  10301  ltxrlt  10321  nn0nepnf  11584  xrltnr  12167  pnfnlt  12176  nltmnf  12177  hashclb  13362  hasheq0  13367  egt2lt3  15154  nthruc  15201  pcgcd1  15804  pc2dvds  15806  ramtcl2  15938  odhash3  18212  xrsmgmdifsgrp  20006  xrsdsreclblem  20015  topnex  21023  pnfnei  21247  mnfnei  21248  zclmncvs  23169  i1f0rn  23669  deg1nn0clb  24070  rgrx0ndm  26721  rgrx0nd  26722  mnfnre2  40136  pnfnre2  40145
  Copyright terms: Public domain W3C validator