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

Theorem nelir 3097
Description: Inference associated with df-nel 3095. (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 3095 . 2 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
31, 2mpbir 234 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2112  wnel 3094
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 210  df-nel 3095
This theorem is referenced by:  ru  3722  prneli  4558  ruv  9054  ruALT  9055  cardprc  9397  pnfnre  10675  mnfnre  10677  eirr  15554  sqrt2irr  15598  lcmfnnval  15962  lcmf0  15972  smndex1n0mnd  18073  nsmndex1  18074  zringndrg  20187  topnex  21605  zfbas  22505  aaliou3  24951  finsumvtxdg2sstep  27343  xrge0iifcnv  31290  bj-0nel1  34390  bj-1nel0  34391  bj-0nelsngl  34408  fmtnoinf  44050  fmtno5nprm  44097  4fppr1  44250  0nodd  44427  2nodd  44429  1neven  44553  2zrngnring  44573
  Copyright terms: Public domain W3C validator