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

Theorem pm2.61ne 2767
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 2765 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370    =/= wne 2648
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 2650
This theorem is referenced by:  pwdom  7574  cantnfle  7991  cantnflem1  8009  cantnf  8013  cantnfleOLD  8021  cantnflem1OLD  8032  cantnfOLD  8035  cdalepw  8477  infmap2  8499  zornn0g  8786  ttukeylem6  8795  msqge0  9973  xrsupsslem  11381  xrinfmsslem  11382  fzoss1  11694  swrdcl  12434  abs1m  12942  fsumcvg3  13325  bezoutlem4  13844  gcdmultiplez  13854  dvdssq  13863  pcdvdsb  14054  pcgcd1  14062  pc2dvds  14064  pcaddlem  14069  qexpz  14082  4sqlem19  14143  prmlem1a  14253  gsumwsubmcl  15636  gsumccat  15639  gsumwmhm  15643  zringlpir  18032  zlpir  18037  mretopd  18829  ufildom1  19632  alexsublem  19749  nmolb2d  20430  nmoi  20440  nmoix  20441  ipcau2  20882  mdegcl  21674  ply1divex  21742  ig1pcl  21781  dgrmulc  21872  mulcxplem  22263  vmacl  22590  efvmacl  22592  vmalelog  22678  padicabv  23013  nmlnoubi  24349  nmblolbii  24352  blocnilem  24357  blocni  24358  ubthlem1  24424  nmbdoplbi  25581  cnlnadjlem7  25630  branmfn  25662  pjbdlni  25706  shatomistici  25918  segcon2  28281  cntzsdrg  29708  lssats  32996  ps-1  33460  3atlem5  33470  lplnnle2at  33524  2llnm3N  33552  lvolnle3at  33565  4atex2  34060  cdlemd5  34185  cdleme21k  34321  cdlemg33b  34690  mapdrvallem2  35629  mapdhcl  35711  hdmapval3N  35825  hdmap10  35827  hdmaprnlem17N  35850  hdmap14lem2a  35854  hdmaplkr  35900  hgmapvv  35913
  Copyright terms: Public domain W3C validator