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

Theorem neli 2885
Description: Inference associated with df-nel 2783. (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 2783 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 219 1 ¬ 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 1977  wnel 2781
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 196  df-nel 2783
This theorem is referenced by:  alephprc  8805  renepnf  9966  renemnf  9967  ltxrlt  9987  nn0nepnf  11248  xrltnr  11829  pnfnlt  11838  nltmnf  11839  hashclb  13011  hasheq0  13015  egt2lt3  14773  nthruc  14819  pcgcd1  15419  pc2dvds  15421  ramtcl2  15553  odhash3  17814  xrsmgmdifsgrp  19602  xrsdsreclblem  19611  pnfnei  20834  mnfnei  20835  zclmncvs  22756  i1f0rn  23255  deg1nn0clb  23654  bj-topnex  32247  rgrx0ndm  40793  rgrx0nd  40794
  Copyright terms: Public domain W3C validator