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

Theorem pm2.61ne 2681
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
pm2.61ne.1  |-  ( A  =  B  ->  ( ps 
<->  ch ) )
pm2.61ne.2  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
pm2.61ne.3  |-  ( ph  ->  ch )
Assertion
Ref Expression
pm2.61ne  |-  ( ph  ->  ps )

Proof of Theorem pm2.61ne
StepHypRef Expression
1 pm2.61ne.2 . . 3  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
21expcom 435 . 2  |-  ( A  =/=  B  ->  ( ph  ->  ps ) )
3 nne 2607 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
4 pm2.61ne.3 . . . 4  |-  ( ph  ->  ch )
5 pm2.61ne.1 . . . 4  |-  ( A  =  B  ->  ( ps 
<->  ch ) )
64, 5syl5ibr 221 . . 3  |-  ( A  =  B  ->  ( ph  ->  ps ) )
73, 6sylbi 195 . 2  |-  ( -.  A  =/=  B  -> 
( ph  ->  ps )
)
82, 7pm2.61i 164 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    =/= wne 2601
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-an 371  df-ne 2603
This theorem is referenced by:  pwdom  7455  cantnfle  7871  cantnflem1  7889  cantnf  7893  cantnfleOLD  7901  cantnflem1OLD  7912  cantnfOLD  7915  cdalepw  8357  infmap2  8379  zornn0g  8666  ttukeylem6  8675  msqge0  9853  xrsupsslem  11261  xrinfmsslem  11262  fzoss1  11568  swrdcl  12307  abs1m  12815  fsumcvg3  13198  bezoutlem4  13717  gcdmultiplez  13727  dvdssq  13736  pcdvdsb  13927  pcgcd1  13935  pc2dvds  13937  pcaddlem  13942  qexpz  13955  4sqlem19  14016  prmlem1a  14126  gsumwsubmcl  15507  gsumccat  15510  gsumwmhm  15514  zringlpir  17881  zlpir  17886  mretopd  18671  ufildom1  19474  alexsublem  19591  nmolb2d  20272  nmoi  20282  nmoix  20283  ipcau2  20724  mdegcl  21515  ply1divex  21583  ig1pcl  21622  dgrmulc  21713  mulcxplem  22104  vmacl  22431  efvmacl  22433  vmalelog  22519  padicabv  22854  nmlnoubi  24147  nmblolbii  24150  blocnilem  24155  blocni  24156  ubthlem1  24222  nmbdoplbi  25379  cnlnadjlem7  25428  branmfn  25460  pjbdlni  25504  shatomistici  25716  segcon2  28087  cntzsdrg  29512  lssats  32497  ps-1  32961  3atlem5  32971  lplnnle2at  33025  2llnm3N  33053  lvolnle3at  33066  4atex2  33561  cdlemd5  33686  cdleme21k  33822  cdlemg33b  34191  mapdrvallem2  35130  mapdhcl  35212  hdmapval3N  35326  hdmap10  35328  hdmaprnlem17N  35351  hdmap14lem2a  35355  hdmaplkr  35401  hgmapvv  35414
  Copyright terms: Public domain W3C validator