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

Theorem pm2.61dne 2628
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 2555 . . 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 2551
This theorem is referenced by:  pm2.61dane  2629  wefrc  4518  wereu2  4521  oe0lem  6694  fisupg  7292  marypha1lem  7374  wdomtr  7477  unxpwdom2  7490  fpwwe2lem13  8451  grur1a  8628  grutsk  8631  fimaxre2  9889  xlesubadd  10775  sqreu  12092  pcxcl  13162  pcmpt  13189  isabvd  15836  lspprat  16153  ordtrest2lem  17190  ordthauslem  17370  fbssint  17792  fclscf  17979  tgptsmscld  18102  ovoliunnul  19271  itg11  19451  i1fadd  19455  fta1g  19958  plydiveu  20083  fta1  20093  mulcxp  20444  cxpsqr  20462  ostth3  21200  subfacp1lem5  24650  frmin  25267  brbtwn2  25559  colinearalg  25564  btwnexch2  25672  limsucncmpi  25910  areacirc  25989  comppfsc  26079  fnemeet2  26088  fnejoin2  26090  sstotbnd2  26175  ssbnd  26189  prdsbnd2  26196  rrncmslem  26233  symggen  27081  atnlt  29429  atlelt  29553  llnnlt  29638  lplnnlt  29680  lvolnltN  29733  pmapglb2N  29886  pmapglb2xN  29887  paddasslem14  29948  cdleme27a  30482
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 2553
  Copyright terms: Public domain W3C validator