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

Theorem pm2.61ne 2521
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 2450 . . 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 1623    =/= wne 2446
This theorem is referenced by:  pwdom  7013  cantnfle  7372  cantnflem1  7391  cantnf  7395  cdalepw  7822  infmap2  7844  zornn0g  8132  ttukeylem6  8141  msqge0  9295  xrsupsslem  10625  xrinfmsslem  10626  fzoss1  10896  swrdcl  11452  abs1m  11819  fsumcvg3  12202  bezoutlem4  12720  gcdmultiplez  12730  dvdssq  12739  pcdvdsb  12921  pcgcd1  12929  pc2dvds  12931  pcaddlem  12936  qexpz  12949  4sqlem19  13010  prmlem1a  13108  gsumwsubmcl  14461  gsumccat  14464  gsumwmhm  14467  zlpir  16444  mretopd  16829  ufildom1  17621  alexsublem  17738  nmolb2d  18227  nmoi  18237  nmoix  18238  ipcau2  18664  mdegcl  19455  ply1divex  19522  ig1pcl  19561  dgrmulc  19652  mulcxplem  20031  vmacl  20356  efvmacl  20358  vmalelog  20444  padicabv  20779  nmlnoubi  21374  nmblolbii  21377  blocnilem  21382  blocni  21383  ubthlem1  21449  nmbdoplbi  22604  cnlnadjlem7  22653  branmfn  22685  pjbdlni  22729  shatomistici  22941  segcon2  24728  cntzsdrg  27510  lssats  29202  ps-1  29666  3atlem5  29676  lplnnle2at  29730  2llnm3N  29758  lvolnle3at  29771  4atex2  30266  cdlemd5  30391  cdleme21k  30527  cdlemg33b  30896  mapdrvallem2  31835  mapdhcl  31917  hdmapval3N  32031  hdmap10  32033  hdmaprnlem17N  32056  hdmap14lem2a  32060  hdmaplkr  32106  hgmapvv  32119
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 2448
  Copyright terms: Public domain W3C validator