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

Theorem pm2.61ne 2775
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 2773 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374    =/= wne 2655
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 2657
This theorem is referenced by:  pwdom  7659  cantnfle  8079  cantnflem1  8097  cantnf  8101  cantnfleOLD  8109  cantnflem1OLD  8120  cantnfOLD  8123  cdalepw  8565  infmap2  8587  zornn0g  8874  ttukeylem6  8883  msqge0  10063  xrsupsslem  11487  xrinfmsslem  11488  fzoss1  11809  swrdcl  12596  abs1m  13117  fsumcvg3  13500  bezoutlem4  14027  gcdmultiplez  14037  dvdssq  14046  pcdvdsb  14240  pcgcd1  14248  pc2dvds  14250  pcaddlem  14255  qexpz  14268  4sqlem19  14329  prmlem1a  14439  gsumwsubmcl  15822  gsumccat  15825  gsumwmhm  15829  zringlpir  18272  zlpir  18277  mretopd  19352  ufildom1  20155  alexsublem  20272  nmolb2d  20953  nmoi  20963  nmoix  20964  ipcau2  21405  mdegcl  22197  ply1divex  22265  ig1pcl  22304  dgrmulc  22395  mulcxplem  22786  vmacl  23113  efvmacl  23115  vmalelog  23201  padicabv  23536  nmlnoubi  25373  nmblolbii  25376  blocnilem  25381  blocni  25382  ubthlem1  25448  nmbdoplbi  26605  cnlnadjlem7  26654  branmfn  26686  pjbdlni  26730  shatomistici  26942  segcon2  29318  cntzsdrg  30745  lssats  33684  ps-1  34148  3atlem5  34158  lplnnle2at  34212  2llnm3N  34240  lvolnle3at  34253  4atex2  34748  cdlemd5  34873  cdleme21k  35009  cdlemg33b  35378  mapdrvallem2  36317  mapdhcl  36399  hdmapval3N  36513  hdmap10  36515  hdmaprnlem17N  36538  hdmap14lem2a  36542  hdmaplkr  36588  hgmapvv  36601
  Copyright terms: Public domain W3C validator