Theorem pm2.61ne 2879

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

Step	Hyp	Ref	Expression
1		pm2.61ne.3	. . 3 |- ( ph -> ch )
2		pm2.61ne.1	. . 3 |- ( A = B -> ( ps <-> ch ) )
3	1, 2	syl5ibr 236	. 2 |- ( A = B -> ( ph -> ps ) )
4		pm2.61ne.2	. . 3 |- ( ( ph /\ A =/= B ) -> ps )
5	4	expcom 451	. 2 |- ( A =/= B -> ( ph -> ps ) )
6	3, 5	pm2.61ine 2877	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   =/= wne 2794

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 197  df-an 386  df-ne 2795

This theorem is referenced by:  pwdom  8112  cantnfle  8568  cantnflem1  8586  cantnf  8590  cdalepw  9018  infmap2  9040  zornn0g  9327  ttukeylem6  9336  msqge0  10549  xrsupsslem  12137  xrinfmsslem  12138  fzoss1  12495  swrdcl  13419  abs1m  14075  fsumcvg3  14460  bezoutlem4  15259  gcdmultiplez  15270  dvdssq  15280  lcmid  15322  pcdvdsb  15573  pcgcd1  15581  pc2dvds  15583  pcaddlem  15592  qexpz  15605  4sqlem19  15667  prmlem1a  15813  gsumwsubmcl  17375  gsumccat  17378  gsumwmhm  17382  zringlpir  19837  mretopd  20896  ufildom1  21730  alexsublem  21848  nmolb2d  22522  nmoi  22532  nmoix  22533  ipcau2  23033  mdegcl  23829  ply1divex  23896  ig1pcl  23935  dgrmulc  24027  mulcxplem  24430  vmacl  24844  efvmacl  24846  vmalelog  24930  padicabv  25319  nmlnoubi  27651  nmblolbii  27654  blocnilem  27659  blocni  27660  ubthlem1  27726  nmbdoplbi  28883  cnlnadjlem7  28932  branmfn  28964  pjbdlni  29008  shatomistici  29220  segcon2  32212  lssats  34299  ps-1  34763  3atlem5  34773  lplnnle2at  34827  2llnm3N  34855  lvolnle3at  34868  4atex2  35363  cdlemd5  35489  cdleme21k  35626  cdlemg33b  35995  mapdrvallem2  36934  mapdhcl  37016  hdmapval3N  37130  hdmap10  37132  hdmaprnlem17N  37155  hdmap14lem2a  37159  hdmaplkr  37205  hgmapvv  37218  cntzsdrg  37772  pfxcl  41386