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

Theorem neli 3130
 Description: Inference associated with df-nel 3129. (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 3129 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 231 1 ¬ 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∈ wcel 2107   ∉ wnel 3128 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 208  df-nel 3129 This theorem is referenced by:  alephprc  9519  pnfnre2  10677  renepnf  10683  renemnf  10684  ltxrlt  10705  nn0nepnf  11969  xrltnr  12509  pnfnlt  12518  nltmnf  12519  hashclb  13714  hasheq0  13719  egt2lt3  15554  nthruc  15600  pcgcd1  16208  pc2dvds  16210  ramtcl2  16342  odhash3  18637  xrsmgmdifsgrp  20517  xrsdsreclblem  20526  topnex  21539  pnfnei  21763  mnfnei  21764  zclmncvs  23686  i1f0rn  24217  deg1nn0clb  24618  rgrx0ndm  27308  rgrx0nd  27309  f1resfz0f1d  32264  gonan0  32542  inaex  40517  mnfnre2  41552  nsmndex1  43987
 Copyright terms: Public domain W3C validator