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

Theorem pm2.61dne 2686
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
StepHypRef Expression
1 pm2.61dne.2 . 2  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
2 nne 2610 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61dne.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
42, 3syl5bi 217 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
51, 4pm2.61d 158 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1364    =/= wne 2604
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-ne 2606
This theorem is referenced by:  pm2.61dane  2687  wefrc  4710  wereu2  4713  oe0lem  6949  fisupg  7556  marypha1lem  7679  wdomtr  7786  unxpwdom2  7799  fpwwe2lem13  8805  grur1a  8982  grutsk  8985  fimaxre2  10274  xlesubadd  11222  cshwidxmod  12436  sqreu  12844  pcxcl  13923  pcmpt  13950  symggen  15969  isabvd  16885  lspprat  17212  mdetralt  18373  ordtrest2lem  18766  ordthauslem  18946  fbssint  19370  fclscf  19557  tgptsmscld  19684  ovoliunnul  20949  itg11  21128  i1fadd  21132  fta1g  21598  plydiveu  21723  fta1  21733  mulcxp  22089  cxpsqr  22107  ostth3  22846  brbtwn2  23086  colinearalg  23091  ordtrest2NEWlem  26288  subfacp1lem5  27002  frmin  27632  btwnexch2  27983  limsucncmpi  28221  areacirc  28414  comppfsc  28504  fnemeet2  28513  fnejoin2  28515  sstotbnd2  28598  ssbnd  28612  prdsbnd2  28619  rrncmslem  28656  clwwisshclww  30396  atnlt  32680  atlelt  32804  llnnlt  32889  lplnnlt  32931  lvolnltN  32984  pmapglb2N  33137  pmapglb2xN  33138  paddasslem14  33199  cdleme27a  33733
  Copyright terms: Public domain W3C validator