Theorem pm2.61dne 2880

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
pm2.61dne.1	|- ( ph -> ( A = B -> ps ) )
pm2.61dne.2	|- ( ph -> ( A =/= B -> ps ) )

Assertion

Ref	Expression
pm2.61dne	|- ( ph -> ps )

Proof of Theorem pm2.61dne

Step	Hyp	Ref	Expression
1		pm2.61dne.2	. 2 |- ( ph -> ( A =/= B -> ps ) )
2		nne 2798	. . 3 |- ( -. A =/= B <-> A = B )
3		pm2.61dne.1	. . 3 |- ( ph -> ( A = B -> ps ) )
4	2, 3	syl5bi 232	. 2 |- ( ph -> ( -. A =/= B -> ps ) )
5	1, 4	pm2.61d 170	1 |- ( ph -> ps )

Syntax hints:   -. wn 3   -> wi 4   = 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-ne 2795

This theorem is referenced by:  pm2.61dane  2881  wefrc  5108  wereu2  5111  oe0lem  7593  fisupg  8208  marypha1lem  8339  fiinfg  8405  wdomtr  8480  unxpwdom2  8493  fpwwe2lem13  9464  grur1a  9641  grutsk  9644  fimaxre2  10969  xlesubadd  12093  cshwidxmod  13549  sqreu  14100  pcxcl  15565  pcmpt  15596  symggen  17890  isabvd  18820  lspprat  19153  mdetralt  20414  ordtrest2lem  21007  ordthauslem  21187  comppfsc  21335  fbssint  21642  fclscf  21829  tgptsmscld  21954  ovoliunnul  23275  itg11  23458  i1fadd  23462  fta1g  23927  plydiveu  24053  fta1  24063  mulcxp  24431  cxpsqrt  24449  ostth3  25327  brbtwn2  25785  colinearalg  25790  clwwisshclwws  26928  ordtrest2NEWlem  29968  subfacp1lem5  31166  frmin  31739  btwnexch2  32130  fnemeet2  32362  fnejoin2  32364  limsucncmpi  32444  areacirc  33505  sstotbnd2  33573  ssbnd  33587  prdsbnd2  33594  rrncmslem  33631  atnlt  34600  atlelt  34724  llnnlt  34809  lplnnlt  34851  lvolnltN  34904  pmapglb2N  35057  pmapglb2xN  35058  paddasslem14  35119  cdleme27a  35655  iccpartigtl  41359