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

Theorem pm2.61dne 2774
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
pm2.61dne.2
Assertion
Ref Expression
pm2.61dne

Proof of Theorem pm2.61dne
StepHypRef Expression
1 pm2.61dne.2 . 2
2 nne 2658 . . 3
3 pm2.61dne.1 . . 3
42, 3syl5bi 217 . 2
51, 4pm2.61d 158 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  pm2.61dane  2775  wefrc  4878  wereu2  4881  oe0lem  7182  fisupg  7788  marypha1lem  7913  wdomtr  8022  unxpwdom2  8035  fpwwe2lem13  9041  grur1a  9218  grutsk  9221  fimaxre2  10516  xlesubadd  11484  cshwidxmod  12774  sqreu  13193  pcxcl  14384  pcmpt  14411  symggen  16495  isabvd  17469  lspprat  17799  mdetralt  19110  ordtrest2lem  19704  ordthauslem  19884  comppfsc  20033  fbssint  20339  fclscf  20526  tgptsmscld  20653  ovoliunnul  21918  itg11  22098  i1fadd  22102  fta1g  22568  plydiveu  22694  fta1  22704  mulcxp  23066  cxpsqrt  23084  ostth3  23823  brbtwn2  24208  colinearalg  24213  clwwisshclww  24807  ordtrest2NEWlem  27904  subfacp1lem5  28628  frmin  29322  btwnexch2  29673  limsucncmpi  29910  areacirc  30112  fnemeet2  30185  fnejoin2  30187  sstotbnd2  30270  ssbnd  30284  prdsbnd2  30291  rrncmslem  30328  atnlt  35038  atlelt  35162  llnnlt  35247  lplnnlt  35289  lvolnltN  35342  pmapglb2N  35495  pmapglb2xN  35496  paddasslem14  35557  cdleme27a  36093
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 2654
  Copyright terms: Public domain W3C validator