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

Theorem pm2.61ine 2780
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 2668 . . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  pm2.61ne  2782  pm2.61iine  2789  rgenz  3933  raaan  3935  raaanv  3936  iinrab2  4388  iinvdif  4397  riinrab  4401  reusv2lem2  4649  reusv6OLD  4658  reusv7OLD  4659  xpriindi  5137  dmxpid  5220  dmxpss  5436  rnxpid  5438  cnvpo  5543  xpcoid  5546  fnprb  6117  fconstfv  6121  xpexr  6721  frxp  6890  suppimacnv  6909  fodomr  7665  wdompwdom  8000  en3lp  8029  inf3lemd  8040  prdom2  8380  iunfictbso  8491  infpssrlem4  8682  1re  9591  dedekindle  9740  00id  9750  nn0lt2  10921  nn01to3  11171  ioorebas  11622  fzfi  12046  ssnn0fi  12058  hash2prde  12478  repswsymballbi  12711  cshw0  12724  cshwmodn  12725  cshwsublen  12726  cshwn  12727  cshwlen  12729  cshwidx0  12735  cshwsidrepswmod0  14433  cshwshashlem1  14434  cshwshashlem2  14435  cshwsdisj  14437  cntzssv  16161  psgnunilem4  16318  mulmarep1gsum2  18843  plyssc  22332  axsegcon  23906  axpaschlem  23919  axlowdimlem16  23936  axcontlem7  23949  axcontlem8  23950  axcontlem12  23954  usgra2edg  24058  usgrcyclnl2  24317  4cycl4dv  24343  1to3vfriswmgra  24683  frgranbnb  24696  numclwwlk5  24789  siii  25444  h1de2ctlem  26149  riesz3i  26657  unierri  26699  dya2iocuni  27894  sibf0  27916  dfpo2  28761  cgrextend  29235  ifscgr  29271  idinside  29311  btwnconn1lem12  29325  btwnconn1  29328  linethru  29380  ovoliunnfl  29633  voliunnfl  29635  volsupnfl  29636  sdrgacs  30755  zlmodzxznm  32179  ax6e2ndeq  32412  bnj1143  32928  bnj571  33043  bnj594  33049  bnj852  33058  bj-xpnzex  33597
  Copyright terms: Public domain W3C validator