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

Theorem pm2.61ine 2707
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 2628 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61ine.1 . . 3  |-  ( A  =  B  ->  ph )
42, 3sylbi 199 . 2  |-  ( -.  A  =/=  B  ->  ph )
51, 4pm2.61i 168 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1444    =/= wne 2622
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 189  df-ne 2624
This theorem is referenced by:  pm2.61ne  2709  pm2.61iine  2714  rgenz  3875  raaan  3877  raaanv  3878  iinrab2  4341  iinvdif  4350  riinrab  4354  reusv2lem2  4605  xpriindi  4971  dmxpid  5054  dmxpss  5268  rnxpid  5270  cnvpo  5374  xpcoid  5377  fnprb  6123  fconstfvOLD  6127  xpexr  6733  frxp  6906  suppimacnv  6925  fodomr  7723  wdompwdom  8093  en3lp  8121  inf3lemd  8132  prdom2  8437  iunfictbso  8545  infpssrlem4  8736  1re  9642  dedekindle  9798  00id  9808  nn0lt2  11000  nn01to3  11257  ioorebas  11736  fzfi  12185  ssnn0fi  12197  hash2prde  12631  repswsymballbi  12883  cshw0  12896  cshwmodn  12897  cshwsublen  12898  cshwn  12899  cshwlen  12901  cshwidx0  12907  dmtrclfv  13082  cshwsidrepswmod0  15065  cshwshashlem1  15066  cshwshashlem2  15067  cshwsdisj  15069  cntzssv  16982  psgnunilem4  17138  mulmarep1gsum2  19599  plyssc  23154  axsegcon  24957  axpaschlem  24970  axlowdimlem16  24987  axcontlem7  25000  axcontlem8  25001  axcontlem12  25005  usgra2edg  25109  usgrcyclnl2  25369  4cycl4dv  25395  1to3vfriswmgra  25735  frgranbnb  25748  numclwwlk5  25840  siii  26494  h1de2ctlem  27208  riesz3i  27715  unierri  27757  dya2iocuni  29105  sibf0  29167  bnj1143  29602  bnj571  29717  bnj594  29723  bnj852  29732  dfpo2  30395  cgrextend  30775  ifscgr  30811  idinside  30851  btwnconn1lem12  30865  btwnconn1  30868  linethru  30920  bj-xpnzex  31552  ovoliunnfl  31982  voliunnfl  31984  volsupnfl  31985  sdrgacs  36067  ax6e2ndeq  36926  usgr2edg  39291  nrhmzr  39926  zlmodzxznm  40343
  Copyright terms: Public domain W3C validator