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