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

Theorem pm2.61ne 2758
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
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.3 . . 3  |-  ( ph  ->  ch )
2 pm2.61ne.1 . . 3  |-  ( A  =  B  ->  ( ps 
<->  ch ) )
31, 2syl5ibr 221 . 2  |-  ( A  =  B  ->  ( ph  ->  ps ) )
4 pm2.61ne.2 . . 3  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
54expcom 435 . 2  |-  ( A  =/=  B  ->  ( ph  ->  ps ) )
63, 5pm2.61ine 2756 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383    =/= wne 2638
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 2640
This theorem is referenced by:  pwdom  7671  cantnfle  8093  cantnflem1  8111  cantnf  8115  cantnfleOLD  8123  cantnflem1OLD  8134  cantnfOLD  8137  cdalepw  8579  infmap2  8601  zornn0g  8888  ttukeylem6  8897  msqge0  10081  xrsupsslem  11508  xrinfmsslem  11509  fzoss1  11833  swrdcl  12627  abs1m  13149  fsumcvg3  13532  bezoutlem4  14160  gcdmultiplez  14170  dvdssq  14179  pcdvdsb  14373  pcgcd1  14381  pc2dvds  14383  pcaddlem  14388  qexpz  14401  4sqlem19  14462  prmlem1a  14573  gsumwsubmcl  15984  gsumccat  15987  gsumwmhm  15991  zringlpir  18489  zlpir  18494  mretopd  19570  ufildom1  20404  alexsublem  20521  nmolb2d  21202  nmoi  21212  nmoix  21213  ipcau2  21654  mdegcl  22446  ply1divex  22514  ig1pcl  22553  dgrmulc  22644  mulcxplem  23041  vmacl  23368  efvmacl  23370  vmalelog  23456  padicabv  23791  nmlnoubi  25687  nmblolbii  25690  blocnilem  25695  blocni  25696  ubthlem1  25762  nmbdoplbi  26919  cnlnadjlem7  26968  branmfn  27000  pjbdlni  27044  shatomistici  27256  segcon2  29730  cntzsdrg  31127  lcmid  31191  lssats  34477  ps-1  34941  3atlem5  34951  lplnnle2at  35005  2llnm3N  35033  lvolnle3at  35046  4atex2  35541  cdlemd5  35667  cdleme21k  35804  cdlemg33b  36173  mapdrvallem2  37112  mapdhcl  37194  hdmapval3N  37308  hdmap10  37310  hdmaprnlem17N  37333  hdmap14lem2a  37337  hdmaplkr  37383  hgmapvv  37396
  Copyright terms: Public domain W3C validator