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

Theorem nelir 3049
Description: Inference associated with df-nel 3047. (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 3047 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbir 231 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2108  wnel 3046
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 207  df-nel 3047
This theorem is referenced by:  ru  3786  ruOLD  3787  prneli  4656  ruv  9642  ruALT  9643  cardprc  10020  pnfnre  11302  mnfnre  11304  eirr  16241  sqrt2irr  16285  lcmfnnval  16661  lcmf0  16671  smndex1n0mnd  18925  nsmndex1  18926  zringndrg  21479  topnex  23003  zfbas  23904  aaliou3  26393  finsumvtxdg2sstep  29567  xrge0iifcnv  33932  bj-0nel1  36954  bj-1nel0  36955  bj-0nelsngl  36972  ruvALT  42679  fmtnoinf  47523  fmtno5nprm  47570  4fppr1  47722  0nodd  48086  2nodd  48088  1neven  48154  2zrngnring  48174
  Copyright terms: Public domain W3C validator