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

Theorem pm2.61dne 2523
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 2450 . . 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 1623    =/= wne 2446
This theorem is referenced by:  pm2.61dane  2524  wefrc  4387  wereu2  4390  oe0lem  6512  fisupg  7105  marypha1lem  7186  wdomtr  7289  unxpwdom2  7302  fpwwe2lem13  8264  grur1a  8441  grutsk  8444  fimaxre2  9702  xlesubadd  10583  sqreu  11844  pcxcl  12913  pcmpt  12940  isabvd  15585  lspprat  15906  ordtrest2lem  16933  ordthauslem  17111  fbssint  17533  fclscf  17720  tgptsmscld  17833  ovoliunnul  18866  itg11  19046  i1fadd  19050  fta1g  19553  plydiveu  19678  fta1  19688  mulcxp  20032  cxpsqr  20050  ostth3  20787  subfacp1lem5  23126  frmin  23653  brbtwn2  23944  colinearalg  23949  btwnexch2  24057  limsucncmpi  24295  areacirc  24343  clscnc  25422  lineval5a  25500  lineval6a  25501  comppfsc  25719  fnemeet2  25728  fnejoin2  25730  sstotbnd2  25910  ssbnd  25924  prdsbnd2  25931  rrncmslem  25968  symggen  26823  atnlt  28876  atlelt  29000  llnnlt  29085  lplnnlt  29127  lvolnltN  29180  pmapglb2N  29333  pmapglb2xN  29334  paddasslem14  29395  cdleme27a  29929
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 2448
  Copyright terms: Public domain W3C validator