NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  pm2.61ine Unicode version

Theorem pm2.61ine 2592
Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
pm2.61ine.1
pm2.61ine.2
Assertion
Ref Expression
pm2.61ine

Proof of Theorem pm2.61ine
StepHypRef Expression
1 pm2.61ine.2 . 2
2 nne 2520 . . 3
3 pm2.61ine.1 . . 3
42, 3sylbi 187 . 2
51, 4pm2.61i 156 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wceq 1642   wne 2516
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 177  df-ne 2518
This theorem is referenced by:  rgenz  3655  raaan  3657  raaanv  3658  iinrab2  4029  riinrab  4041  nnsucelr  4428  lenltfin  4469  tfincl  4492  tfin11  4493  tfinltfinlem1  4500  tfinltfin  4501  vfinncvntnn  4548  dmxpid  4924  dmxpss  5052  rnxpid  5054  xpexr  5109  fconstfv  5456  mapsspm  6021  mapsspw  6022  enadj  6060  nc0le1  6216
  Copyright terms: Public domain W3C validator