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

Theorem pm2.61ine 2643
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 2571 . . 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 1649    =/= wne 2567
This theorem is referenced by:  rgenz  3693  raaan  3695  raaanv  3696  iinrab2  4114  riinrab  4126  reusv2lem2  4684  reusv6OLD  4693  reusv7OLD  4694  xpriindi  4970  dmxpid  5048  dmxpss  5259  rnxpid  5261  xpexr  5266  cnvpo  5369  xpcoid  5374  fconstfv  5913  frxp  6415  fodomr  7217  wdompwdom  7502  inf3lemd  7538  en3lp  7628  prdom2  7846  iunfictbso  7951  infpssrlem4  8142  1re  9046  00id  9197  ioorebas  10962  fzfi  11266  hash2prde  11643  cntzssv  15082  plyssc  20072  usgra2edg  21355  usgrcyclnl2  21581  4cycl4dv  21607  siii  22307  h1de2ctlem  23010  riesz3i  23518  unierri  23560  dya2iocuni  24586  sibf0  24602  dedekindle  25141  dfpo2  25326  axsegcon  25770  axpaschlem  25783  axlowdimlem16  25800  axcontlem7  25813  axcontlem8  25814  axcontlem12  25818  cgrextend  25846  ifscgr  25882  idinside  25922  btwnconn1lem12  25936  btwnconn1  25939  linethru  25991  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  psgnunilem4  27288  sdrgacs  27377  1to3vfriswmgra  28111  frgranbnb  28124  a9e2ndeq  28357  bnj1143  28867  bnj571  28983  bnj594  28989  bnj852  28998
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 2569
  Copyright terms: Public domain W3C validator