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

Theorem neli 3068
Description: Inference associated with df-nel 3067. (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 3067 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbi 233 1 ¬ 𝐴𝐵
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3  wcel 2146  wnel 3066
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This proof depends on definitions:  df-bi 210  df-nel 3067
This theorem is used by:  alephprc  10099  pnfnre2  11268  renepnf  11274  renemnf  11275  ltxrlt  11297  nn0nepnf  12602  xrltnr  13162  pnfnlt  13171  nltmnf  13172  f1resfz0f1d  13840  hashclb  14414  hasheq0  14419  egt2lt3  16286  nthruc  16332  pcgcd1  16961  pc2dvds  16963  ramtcl2  17095  nsmndex1  19014  odhash3  19692  xrsmgmdifsgrp  21611  xrsdsreclblem  21615  topnex  23205  pnfnei  23429  mnfnei  23430  zclmncvs  25360  i1f0rn  25894  deg1nn0clb  26300  rgrx0ndm  30003  rgrx0nd  30004  nowisdomv  30898  ply1coedeg  33945  trisecnconstr  34248  gonan0  35923  inaex  45067  mnfnre2  46171  nthrucw  47667  fonex  49704
  Copyright terms: Public domain W3C validator