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

Theorem pm2.61dne 2784
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 2668 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61dne.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
42, 3syl5bi 217 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
51, 4pm2.61d 158 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1379    =/= wne 2662
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 2664
This theorem is referenced by:  pm2.61dane  2785  wefrc  4873  wereu2  4876  oe0lem  7163  fisupg  7767  marypha1lem  7892  wdomtr  8000  unxpwdom2  8013  fpwwe2lem13  9019  grur1a  9196  grutsk  9199  fimaxre2  10490  xlesubadd  11454  cshwidxmod  12736  sqreu  13155  pcxcl  14242  pcmpt  14269  symggen  16298  isabvd  17264  lspprat  17594  mdetralt  18893  ordtrest2lem  19486  ordthauslem  19666  fbssint  20090  fclscf  20277  tgptsmscld  20404  ovoliunnul  21669  itg11  21849  i1fadd  21853  fta1g  22319  plydiveu  22444  fta1  22454  mulcxp  22810  cxpsqrt  22828  ostth3  23567  brbtwn2  23900  colinearalg  23905  clwwisshclww  24499  ordtrest2NEWlem  27556  subfacp1lem5  28284  frmin  28915  btwnexch2  29266  limsucncmpi  29503  areacirc  29705  comppfsc  29795  fnemeet2  29804  fnejoin2  29806  sstotbnd2  29889  ssbnd  29903  prdsbnd2  29910  rrncmslem  29947  atnlt  34119  atlelt  34243  llnnlt  34328  lplnnlt  34370  lvolnltN  34423  pmapglb2N  34576  pmapglb2xN  34577  paddasslem14  34638  cdleme27a  35172
  Copyright terms: Public domain W3C validator