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

Theorem nelir 3030
Description: Inference associated with df-nel 3028. (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 3028 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbir 221 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2131  wnel 3027
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 197  df-nel 3028
This theorem is referenced by:  ru  3567  prneli  4339  snnexOLD  7124  ruv  8664  ruALT  8665  cardprc  8988  pnfnre  10265  mnfnre  10266  wrdlndm  13499  eirr  15124  sqrt2irr  15170  lcmfnnval  15531  lcmf0  15541  zringndrg  20032  topnex  20994  zfbas  21893  aaliou3  24297  finsumvtxdg2sstep  26647  clwwlkn0OLD  27149  xrge0iifcnv  30280  bj-0nel1  33238  bj-1nel0  33239  bj-0nelsngl  33257  fmtnoinf  41950  fmtno5nprm  41997  0nodd  42312  2nodd  42314  1neven  42434  2zrngnring  42454
  Copyright terms: Public domain W3C validator