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

Theorem nelir 3126
Description: Inference associated with df-nel 3124. (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 3124 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbir 232 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2105  wnel 3123
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 3124
This theorem is referenced by:  ru  3770  prneli  4587  ruv  9055  ruALT  9056  cardprc  9398  pnfnre  10671  mnfnre  10673  wrdlndmOLD  13870  eirr  15548  sqrt2irr  15592  lcmfnnval  15958  lcmf0  15968  zringndrg  20567  topnex  21534  zfbas  22434  aaliou3  24869  finsumvtxdg2sstep  27259  xrge0iifcnv  31076  bj-0nel1  34163  bj-1nel0  34164  bj-0nelsngl  34181  fmtnoinf  43545  fmtno5nprm  43592  4fppr1  43747  0nodd  43924  2nodd  43926  smndex1n0mnd  43982  nsmndex1  43983  1neven  44101  2zrngnring  44121
  Copyright terms: Public domain W3C validator