New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  pm2.61ine GIF 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 (A = Bφ)
pm2.61ine.2 (ABφ)
Assertion
Ref Expression
pm2.61ine φ

Proof of Theorem pm2.61ine
StepHypRef Expression
1 pm2.61ine.2 . 2 (ABφ)
2 nne 2520 . . 3 ABA = B)
3 pm2.61ine.1 . . 3 (A = Bφ)
42, 3sylbi 187 . 2 ABφ)
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