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

Theorem pm2.61ine 2767
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 2655 . . 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 1398    =/= wne 2649
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 2651
This theorem is referenced by:  pm2.61ne  2769  pm2.61iine  2776  rgenz  3923  raaan  3925  raaanv  3926  iinrab2  4378  iinvdif  4387  riinrab  4391  reusv2lem2  4639  reusv6OLD  4648  reusv7OLD  4649  xpriindi  5128  dmxpid  5211  dmxpss  5423  rnxpid  5425  cnvpo  5528  xpcoid  5531  fnprb  6106  fconstfvOLD  6109  xpexr  6713  frxp  6883  suppimacnv  6902  fodomr  7661  wdompwdom  7996  en3lp  8024  inf3lemd  8035  prdom2  8375  iunfictbso  8486  infpssrlem4  8677  1re  9584  dedekindle  9734  00id  9744  nn0lt2  10923  nn01to3  11176  ioorebas  11629  fzfi  12067  ssnn0fi  12079  hash2prde  12503  repswsymballbi  12746  cshw0  12759  cshwmodn  12760  cshwsublen  12761  cshwn  12762  cshwlen  12764  cshwidx0  12770  dmtrclfv  12939  cshwsidrepswmod0  14666  cshwshashlem1  14667  cshwshashlem2  14668  cshwsdisj  14670  cntzssv  16568  psgnunilem4  16724  mulmarep1gsum2  19246  plyssc  22766  axsegcon  24435  axpaschlem  24448  axlowdimlem16  24465  axcontlem7  24478  axcontlem8  24479  axcontlem12  24483  usgra2edg  24587  usgrcyclnl2  24846  4cycl4dv  24872  1to3vfriswmgra  25212  frgranbnb  25225  numclwwlk5  25317  siii  25969  h1de2ctlem  26674  riesz3i  27182  unierri  27224  dya2iocuni  28494  sibf0  28543  dfpo2  29428  cgrextend  29889  ifscgr  29925  idinside  29965  btwnconn1lem12  29979  btwnconn1  29982  linethru  30034  ovoliunnfl  30299  voliunnfl  30301  volsupnfl  30302  sdrgacs  31394  nrhmzr  32952  zlmodzxznm  33371  ax6e2ndeq  33745  bnj1143  34269  bnj571  34384  bnj594  34390  bnj852  34399  bj-xpnzex  34936
  Copyright terms: Public domain W3C validator