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

Theorem neli 3048
Description: Inference associated with df-nel 3047. (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 3047 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 230 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2108  wnel 3046
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 207  df-nel 3047
This theorem is referenced by:  alephprc  10139  pnfnre2  11303  renepnf  11309  renemnf  11310  ltxrlt  11331  nn0nepnf  12607  xrltnr  13161  pnfnlt  13170  nltmnf  13171  hashclb  14397  hasheq0  14402  egt2lt3  16242  nthruc  16288  pcgcd1  16915  pc2dvds  16917  ramtcl2  17049  nsmndex1  18926  odhash3  19594  xrsmgmdifsgrp  21421  xrsdsreclblem  21430  topnex  23003  pnfnei  23228  mnfnei  23229  zclmncvs  25182  i1f0rn  25717  deg1nn0clb  26129  rgrx0ndm  29611  rgrx0nd  29612  f1resfz0f1d  35119  gonan0  35397  inaex  44316  mnfnre2  45407
  Copyright terms: Public domain W3C validator