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

Theorem neli 3076
Description: Inference associated with df-nel 3075. (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 3075 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 222 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2157  wnel 3074
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 199  df-nel 3075
This theorem is referenced by:  alephprc  9208  renepnf  10376  renemnf  10377  ltxrlt  10398  nn0nepnf  11660  xrltnr  12200  pnfnlt  12209  nltmnf  12210  hashclb  13399  hasheq0  13404  egt2lt3  15270  nthruc  15317  pcgcd1  15914  pc2dvds  15916  ramtcl2  16048  odhash3  18304  xrsmgmdifsgrp  20105  xrsdsreclblem  20114  topnex  21129  pnfnei  21353  mnfnei  21354  zclmncvs  23275  i1f0rn  23790  deg1nn0clb  24191  rgrx0ndm  26843  rgrx0nd  26844  mnfnre2  40362  pnfnre2  40371
  Copyright terms: Public domain W3C validator