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

Theorem pm2.61dne 2536
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 2463 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61dne.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
42, 3syl5bi 208 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
51, 4pm2.61d 150 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  pm2.61dane  2537  wefrc  4403  wereu2  4406  oe0lem  6528  fisupg  7121  marypha1lem  7202  wdomtr  7305  unxpwdom2  7318  fpwwe2lem13  8280  grur1a  8457  grutsk  8460  fimaxre2  9718  xlesubadd  10599  sqreu  11860  pcxcl  12929  pcmpt  12956  isabvd  15601  lspprat  15922  ordtrest2lem  16949  ordthauslem  17127  fbssint  17549  fclscf  17736  tgptsmscld  17849  ovoliunnul  18882  itg11  19062  i1fadd  19066  fta1g  19569  plydiveu  19694  fta1  19704  mulcxp  20048  cxpsqr  20066  ostth3  20803  subfacp1lem5  23730  frmin  24313  brbtwn2  24605  colinearalg  24610  btwnexch2  24718  limsucncmpi  24956  areacirc  25034  clscnc  26113  lineval5a  26191  lineval6a  26192  comppfsc  26410  fnemeet2  26419  fnejoin2  26421  sstotbnd2  26601  ssbnd  26615  prdsbnd2  26622  rrncmslem  26659  symggen  27514  atnlt  30125  atlelt  30249  llnnlt  30334  lplnnlt  30376  lvolnltN  30429  pmapglb2N  30582  pmapglb2xN  30583  paddasslem14  30644  cdleme27a  31178
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2461
  Copyright terms: Public domain W3C validator