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

Theorem pm2.61ine 2522
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  ->  ph )
pm2.61ine.2  |-  ( A  =/=  B  ->  ph )
Assertion
Ref Expression
pm2.61ine  |-  ph

Proof of Theorem pm2.61ine
StepHypRef Expression
1 pm2.61ine.2 . 2  |-  ( A  =/=  B  ->  ph )
2 nne 2450 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61ine.1 . . 3  |-  ( A  =  B  ->  ph )
42, 3sylbi 187 . 2  |-  ( -.  A  =/=  B  ->  ph )
51, 4pm2.61i 156 1  |-  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  rgenz  3559  raaan  3561  raaanv  3562  iinrab2  3965  riinrab  3977  reusv2lem2  4536  reusv6OLD  4545  reusv7OLD  4546  xpriindi  4822  dmxpid  4898  dmxpss  5107  rnxpid  5109  xpexr  5114  cnvpo  5213  fconstfv  5734  frxp  6225  fodomr  7012  wdompwdom  7292  inf3lemd  7328  en3lp  7418  prdom2  7636  iunfictbso  7741  infpssrlem4  7932  1re  8837  00id  8987  ioorebas  10745  fzfi  11034  cntzssv  14804  plyssc  19582  siii  21431  h1de2ctlem  22134  riesz3i  22642  unierri  22684  dedekindle  24083  dfpo2  24112  axsegcon  24555  axpaschlem  24568  axlowdimlem16  24585  axcontlem7  24598  axcontlem8  24599  axcontlem12  24603  cgrextend  24631  ifscgr  24667  idinside  24707  btwnconn1lem12  24721  btwnconn1  24724  linethru  24776  rnintintrn  25126  fsumprd  25329  hdrmp  25706  clscnc  26010  lineval12a  26084  lineval2a  26085  lineval2b  26086  lineval4a  26087  isconcl5a  26101  isconcl5ab  26102  sgplpte21d1  26139  sgplpte21d2  26140  segline  26141  segray  26155  rayline  26156  psgnunilem4  27420  sdrgacs  27509  1to3vfriswmgra  28185  a9e2ndeq  28325  bnj1143  28822  bnj571  28938  bnj594  28944  bnj852  28953
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2448
  Copyright terms: Public domain W3C validator