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 426 . 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 214 . . 3  |-  ( A  =  B  ->  ( ph  ->  ps ) )
73, 6sylbi 189 . 2  |-  ( -.  A  =/=  B  -> 
( ph  ->  ps )
)
82, 7pm2.61i 159 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    =/= wne 2601
This theorem is referenced by:  pwdom  7261  cantnfle  7628  cantnflem1  7647  cantnf  7651  cdalepw  8078  infmap2  8100  zornn0g  8387  ttukeylem6  8396  msqge0  9551  xrsupsslem  10887  xrinfmsslem  10888  fzoss1  11164  swrdcl  11768  abs1m  12141  fsumcvg3  12525  bezoutlem4  13043  gcdmultiplez  13053  dvdssq  13062  pcdvdsb  13244  pcgcd1  13252  pc2dvds  13254  pcaddlem  13259  qexpz  13272  4sqlem19  13333  prmlem1a  13431  gsumwsubmcl  14786  gsumccat  14789  gsumwmhm  14792  zlpir  16773  mretopd  17158  ufildom1  17960  alexsublem  18077  nmolb2d  18754  nmoi  18764  nmoix  18765  ipcau2  19193  mdegcl  19994  ply1divex  20061  ig1pcl  20100  dgrmulc  20191  mulcxplem  20577  vmacl  20903  efvmacl  20905  vmalelog  20991  padicabv  21326  nmlnoubi  22299  nmblolbii  22302  blocnilem  22307  blocni  22308  ubthlem1  22374  nmbdoplbi  23529  cnlnadjlem7  23578  branmfn  23610  pjbdlni  23654  shatomistici  23866  segcon2  26041  cntzsdrg  27489  lssats  29872  ps-1  30336  3atlem5  30346  lplnnle2at  30400  2llnm3N  30428  lvolnle3at  30441  4atex2  30936  cdlemd5  31061  cdleme21k  31197  cdlemg33b  31566  mapdrvallem2  32505  mapdhcl  32587  hdmapval3N  32701  hdmap10  32703  hdmaprnlem17N  32726  hdmap14lem2a  32730  hdmaplkr  32776  hgmapvv  32789
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 179  df-an 362  df-ne 2603
  Copyright terms: Public domain W3C validator