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

Theorem nelir 2793
Description: Inference associated with df-nel 2655. (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 2655 . 2
31, 2mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  e.wcel 1818  e/wnel 2653
This theorem is referenced by:  ru  3326  snnex  6606  ruv  8048  ruALT  8049  cardprc  8382  pnfnre  9656  mnfnre  9657  eirr  13938  sqrt2irr  13982  zfbas  20397  aaliou3  22747  xrge0iifcnv  27915  0nodd  32498  2nodd  32500  1neven  32738  2zrngnring  32758  AnelBC  33158  bj-0nel1  34509  bj-1nel0  34510  bj-0nelsngl  34529
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 185  df-nel 2655
  Copyright terms: Public domain W3C validator