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

Theorem neli 2928
Description: Inference associated with df-nel 2927. (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 2927 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 220 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2030  wnel 2926
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 2927
This theorem is referenced by:  alephprc  8960  renepnf  10125  renemnf  10126  ltxrlt  10146  nn0nepnf  11409  xrltnr  11991  pnfnlt  12000  nltmnf  12001  hashclb  13187  hasheq0  13192  egt2lt3  14978  nthruc  15025  pcgcd1  15628  pc2dvds  15630  ramtcl2  15762  odhash3  18037  xrsmgmdifsgrp  19831  xrsdsreclblem  19840  topnex  20848  pnfnei  21072  mnfnei  21073  zclmncvs  22994  i1f0rn  23494  deg1nn0clb  23895  rgrx0ndm  26545  rgrx0nd  26546  mnfnre2  39932  pnfnre2  39941
  Copyright terms: Public domain W3C validator