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

Theorem pm2.61ine 2737
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 2624 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61ine.1 . . 3  |-  ( A  =  B  ->  ph )
42, 3sylbi 198 . 2  |-  ( -.  A  =/=  B  ->  ph )
51, 4pm2.61i 167 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437    =/= wne 2618
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 188  df-ne 2620
This theorem is referenced by:  pm2.61ne  2739  pm2.61iine  2746  rgenz  3903  raaan  3905  raaanv  3906  iinrab2  4359  iinvdif  4368  riinrab  4372  reusv2lem2  4622  xpriindi  4986  dmxpid  5069  dmxpss  5283  rnxpid  5285  cnvpo  5389  xpcoid  5392  fnprb  6134  fconstfvOLD  6138  xpexr  6743  frxp  6913  suppimacnv  6932  fodomr  7725  wdompwdom  8095  en3lp  8123  inf3lemd  8134  prdom2  8438  iunfictbso  8545  infpssrlem4  8736  1re  9642  dedekindle  9798  00id  9808  nn0lt2  11000  nn01to3  11257  ioorebas  11736  fzfi  12184  ssnn0fi  12196  hash2prde  12628  repswsymballbi  12873  cshw0  12886  cshwmodn  12887  cshwsublen  12888  cshwn  12889  cshwlen  12891  cshwidx0  12897  dmtrclfv  13070  cshwsidrepswmod0  15052  cshwshashlem1  15053  cshwshashlem2  15054  cshwsdisj  15056  cntzssv  16969  psgnunilem4  17125  mulmarep1gsum2  19585  plyssc  23140  axsegcon  24943  axpaschlem  24956  axlowdimlem16  24973  axcontlem7  24986  axcontlem8  24987  axcontlem12  24991  usgra2edg  25095  usgrcyclnl2  25354  4cycl4dv  25380  1to3vfriswmgra  25720  frgranbnb  25733  numclwwlk5  25825  siii  26479  h1de2ctlem  27193  riesz3i  27700  unierri  27742  dya2iocuni  29100  sibf0  29162  bnj1143  29597  bnj571  29712  bnj594  29718  bnj852  29727  dfpo2  30389  cgrextend  30767  ifscgr  30803  idinside  30843  btwnconn1lem12  30857  btwnconn1  30860  linethru  30912  bj-xpnzex  31507  ovoliunnfl  31895  voliunnfl  31897  volsupnfl  31898  sdrgacs  35986  ax6e2ndeq  36783  usgr2edg  38913  nrhmzr  39144  zlmodzxznm  39563
  Copyright terms: Public domain W3C validator