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

Theorem nelir 2882
Description: Inference associated with df-nel 2779. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
nelir.1 ¬ 𝐴𝐵
Assertion
Ref Expression
nelir 𝐴𝐵

Proof of Theorem nelir
StepHypRef Expression
1 nelir.1 . 2 ¬ 𝐴𝐵
2 df-nel 2779 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbir 219 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 1976  wnel 2777
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 195  df-nel 2779
This theorem is referenced by:  ru  3397  prneli  4146  snnex  6836  ruv  8364  ruALT  8365  cardprc  8663  pnfnre  9934  mnfnre  9935  wrdlndm  13119  eirr  14715  sqrt2irr  14760  lcmfnnval  15118  lcmf0  15128  zfbas  21449  aaliou3  23824  xrge0iifcnv  29110  bj-0nel1  31933  bj-1nel0  31934  bj-0nelsngl  31952  bj-topnex  32047  fmtnoinf  39788  fmtno5nprm  39835  clwwlksn0  41213  0nodd  41599  2nodd  41601  1neven  41721  2zrngnring  41741
  Copyright terms: Public domain W3C validator