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

Theorem neli 3125
Description: Inference associated with df-nel 3124. (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 3124 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 231 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2105  wnel 3123
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 208  df-nel 3124
This theorem is referenced by:  alephprc  9514  pnfnre2  10672  renepnf  10678  renemnf  10679  ltxrlt  10700  nn0nepnf  11964  xrltnr  12504  pnfnlt  12513  nltmnf  12514  hashclb  13709  hasheq0  13714  egt2lt3  15549  nthruc  15595  pcgcd1  16203  pc2dvds  16205  ramtcl2  16337  odhash3  18632  xrsmgmdifsgrp  20512  xrsdsreclblem  20521  topnex  21534  pnfnei  21758  mnfnei  21759  zclmncvs  23681  i1f0rn  24212  deg1nn0clb  24613  rgrx0ndm  27303  rgrx0nd  27304  f1resfz0f1d  32259  gonan0  32537  inaex  40513  mnfnre2  41548  nsmndex1  43983
  Copyright terms: Public domain W3C validator