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

Theorem pm2.61ine 2761
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 2650 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61ine.1 . . 3  |-  ( A  =  B  ->  ph )
42, 3sylbi 195 . 2  |-  ( -.  A  =/=  B  ->  ph )
51, 4pm2.61i 164 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2644
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 185  df-ne 2646
This theorem is referenced by:  pm2.61ne  2763  pm2.61iine  2770  rgenz  3886  raaan  3888  raaanv  3889  iinrab2  4334  iinvdif  4343  riinrab  4347  reusv2lem2  4595  reusv6OLD  4604  reusv7OLD  4605  xpriindi  5077  dmxpid  5160  dmxpss  5370  rnxpid  5372  cnvpo  5476  xpcoid  5479  fnprb  6038  fconstfv  6042  xpexr  6621  frxp  6785  suppimacnv  6804  fodomr  7565  wdompwdom  7897  en3lp  7926  inf3lemd  7937  prdom2  8277  iunfictbso  8388  infpssrlem4  8579  1re  9489  dedekindle  9638  00id  9648  ioorebas  11501  fzfi  11904  hash2prde  12290  repswsymballbi  12529  cshw0  12542  cshwmodn  12543  cshwsublen  12544  cshwn  12545  cshwlen  12547  cshwidx0  12553  cshwsidrepswmod0  14232  cshwshashlem1  14233  cshwshashlem2  14234  cshwsdisj  14236  cntzssv  15957  psgnunilem4  16114  mulmarep1gsum2  18505  plyssc  21794  axsegcon  23318  axpaschlem  23331  axlowdimlem16  23348  axcontlem7  23361  axcontlem8  23362  axcontlem12  23366  usgra2edg  23446  usgrcyclnl2  23672  4cycl4dv  23698  siii  24398  h1de2ctlem  25103  riesz3i  25611  unierri  25653  dya2iocuni  26835  sibf0  26857  dfpo2  27702  cgrextend  28176  ifscgr  28212  idinside  28252  btwnconn1lem12  28266  btwnconn1  28269  linethru  28321  ovoliunnfl  28574  voliunnfl  28576  volsupnfl  28577  sdrgacs  29699  nn0lt2  30327  nn01to3  30328  1to3vfriswmgra  30740  frgranbnb  30753  numclwwlk5  30846  ssnn0fi  30887  zlmodzxznm  31149  ax6e2ndeq  31571  bnj1143  32087  bnj571  32202  bnj594  32208  bnj852  32217  bj-xpnzex  32754
  Copyright terms: Public domain W3C validator