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

Theorem pm2.61dne 2688
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 2612 . . 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 1369    =/= wne 2606
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 2608
This theorem is referenced by:  pm2.61dane  2689  wefrc  4714  wereu2  4717  oe0lem  6953  fisupg  7560  marypha1lem  7683  wdomtr  7790  unxpwdom2  7803  fpwwe2lem13  8809  grur1a  8986  grutsk  8989  fimaxre2  10278  xlesubadd  11226  cshwidxmod  12440  sqreu  12848  pcxcl  13927  pcmpt  13954  symggen  15976  isabvd  16905  lspprat  17234  mdetralt  18414  ordtrest2lem  18807  ordthauslem  18987  fbssint  19411  fclscf  19598  tgptsmscld  19725  ovoliunnul  20990  itg11  21169  i1fadd  21173  fta1g  21639  plydiveu  21764  fta1  21774  mulcxp  22130  cxpsqr  22148  ostth3  22887  brbtwn2  23151  colinearalg  23156  ordtrest2NEWlem  26352  subfacp1lem5  27072  frmin  27703  btwnexch2  28054  limsucncmpi  28291  areacirc  28489  comppfsc  28579  fnemeet2  28588  fnejoin2  28590  sstotbnd2  28673  ssbnd  28687  prdsbnd2  28694  rrncmslem  28731  clwwisshclww  30471  atnlt  32958  atlelt  33082  llnnlt  33167  lplnnlt  33209  lvolnltN  33262  pmapglb2N  33415  pmapglb2xN  33416  paddasslem14  33477  cdleme27a  34011
  Copyright terms: Public domain W3C validator