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

Theorem pm2.61dne 2644
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 2571 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61dne.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
42, 3syl5bi 209 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
51, 4pm2.61d 152 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2567
This theorem is referenced by:  pm2.61dane  2645  wefrc  4536  wereu2  4539  oe0lem  6716  fisupg  7314  marypha1lem  7396  wdomtr  7499  unxpwdom2  7512  fpwwe2lem13  8473  grur1a  8650  grutsk  8653  fimaxre2  9912  xlesubadd  10798  sqreu  12119  pcxcl  13189  pcmpt  13216  isabvd  15863  lspprat  16180  ordtrest2lem  17221  ordthauslem  17401  fbssint  17823  fclscf  18010  tgptsmscld  18133  ovoliunnul  19356  itg11  19536  i1fadd  19540  fta1g  20043  plydiveu  20168  fta1  20178  mulcxp  20529  cxpsqr  20547  ostth3  21285  subfacp1lem5  24823  frmin  25456  brbtwn2  25748  colinearalg  25753  btwnexch2  25861  limsucncmpi  26099  areacirc  26187  comppfsc  26277  fnemeet2  26286  fnejoin2  26288  sstotbnd2  26373  ssbnd  26387  prdsbnd2  26394  rrncmslem  26431  symggen  27279  atnlt  29796  atlelt  29920  llnnlt  30005  lplnnlt  30047  lvolnltN  30100  pmapglb2N  30253  pmapglb2xN  30254  paddasslem14  30315  cdleme27a  30849
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 178  df-ne 2569
  Copyright terms: Public domain W3C validator