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

Theorem pm2.61ine 2680
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 2605 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61ine.1 . . 3  |-  ( A  =  B  ->  ph )
42, 3sylbi 188 . 2  |-  ( -.  A  =/=  B  ->  ph )
51, 4pm2.61i 158 1  |-  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2599
This theorem is referenced by:  rgenz  3733  raaan  3735  raaanv  3736  iinrab2  4154  riinrab  4166  reusv2lem2  4725  reusv6OLD  4734  reusv7OLD  4735  xpriindi  5011  dmxpid  5089  dmxpss  5300  rnxpid  5302  xpexr  5307  cnvpo  5410  xpcoid  5415  fconstfv  5954  frxp  6456  fodomr  7258  wdompwdom  7546  inf3lemd  7582  en3lp  7672  prdom2  7890  iunfictbso  7995  infpssrlem4  8186  1re  9090  00id  9241  ioorebas  11006  fzfi  11311  hash2prde  11688  cntzssv  15127  plyssc  20119  usgra2edg  21402  usgrcyclnl2  21628  4cycl4dv  21654  siii  22354  h1de2ctlem  23057  riesz3i  23565  unierri  23607  dya2iocuni  24633  sibf0  24649  dedekindle  25188  dfpo2  25378  axsegcon  25866  axpaschlem  25879  axlowdimlem16  25896  axcontlem7  25909  axcontlem8  25910  axcontlem12  25914  cgrextend  25942  ifscgr  25978  idinside  26018  btwnconn1lem12  26032  btwnconn1  26035  linethru  26087  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  psgnunilem4  27397  sdrgacs  27486  cshwssizelem3  28282  cshwssizelem4a  28283  cshwsdisj  28285  1to3vfriswmgra  28397  frgranbnb  28410  a9e2ndeq  28646  bnj1143  29161  bnj571  29277  bnj594  29283  bnj852  29292
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 178  df-ne 2601
  Copyright terms: Public domain W3C validator