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

Theorem pm2.61ne 2534
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 424 . 2  |-  ( A  =/=  B  ->  ( ph  ->  ps ) )
3 nne 2463 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
4 pm2.61ne.3 . . . 4  |-  ( ph  ->  ch )
5 pm2.61ne.1 . . . 4  |-  ( A  =  B  ->  ( ps 
<->  ch ) )
64, 5syl5ibr 212 . . 3  |-  ( A  =  B  ->  ( ph  ->  ps ) )
73, 6sylbi 187 . 2  |-  ( -.  A  =/=  B  -> 
( ph  ->  ps )
)
82, 7pm2.61i 156 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    =/= wne 2459
This theorem is referenced by:  pwdom  7029  cantnfle  7388  cantnflem1  7407  cantnf  7411  cdalepw  7838  infmap2  7860  zornn0g  8148  ttukeylem6  8157  msqge0  9311  xrsupsslem  10641  xrinfmsslem  10642  fzoss1  10912  swrdcl  11468  abs1m  11835  fsumcvg3  12218  bezoutlem4  12736  gcdmultiplez  12746  dvdssq  12755  pcdvdsb  12937  pcgcd1  12945  pc2dvds  12947  pcaddlem  12952  qexpz  12965  4sqlem19  13026  prmlem1a  13124  gsumwsubmcl  14477  gsumccat  14480  gsumwmhm  14483  zlpir  16460  mretopd  16845  ufildom1  17637  alexsublem  17754  nmolb2d  18243  nmoi  18253  nmoix  18254  ipcau2  18680  mdegcl  19471  ply1divex  19538  ig1pcl  19577  dgrmulc  19668  mulcxplem  20047  vmacl  20372  efvmacl  20374  vmalelog  20460  padicabv  20795  nmlnoubi  21390  nmblolbii  21393  blocnilem  21398  blocni  21399  ubthlem1  21465  nmbdoplbi  22620  cnlnadjlem7  22669  branmfn  22701  pjbdlni  22745  shatomistici  22957  segcon2  24800  cntzsdrg  27613  lssats  29824  ps-1  30288  3atlem5  30298  lplnnle2at  30352  2llnm3N  30380  lvolnle3at  30393  4atex2  30888  cdlemd5  31013  cdleme21k  31149  cdlemg33b  31518  mapdrvallem2  32457  mapdhcl  32539  hdmapval3N  32653  hdmap10  32655  hdmaprnlem17N  32678  hdmap14lem2a  32682  hdmaplkr  32728  hgmapvv  32741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-ne 2461
  Copyright terms: Public domain W3C validator