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

Theorem neli 2789
Description: Inference associated with df-nel 2687. (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 2687 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 218 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 1938  wnel 2685
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 195  df-nel 2687
This theorem is referenced by:  alephprc  8681  renepnf  9842  renemnf  9843  ltxrlt  9858  xrltnr  11700  pnfnlt  11709  nltmnf  11710  hashclb  12876  hasheq0  12880  egt2lt3  14642  nthruc  14688  pcgcd1  15303  pc2dvds  15305  ramtcl2  15437  odhash3  17719  xrsmgmdifsgrp  19506  xrsdsreclblem  19515  pnfnei  20737  mnfnei  20738  i1f0rn  23130  deg1nn0clb  23529  bj-topnex  32078  nn0nepnf  40311  rgrx0ndm  40898  rgrx0nd  40899
  Copyright terms: Public domain W3C validator