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

Theorem pm2.61dne 2748
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 2631 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
3 pm2.61dne.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
42, 3syl5bi 220 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
51, 4pm2.61d 161 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437    =/= wne 2625
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 188  df-ne 2627
This theorem is referenced by:  pm2.61dane  2749  wefrc  4848  wereu2  4851  oe0lem  7223  fisupg  7825  marypha1lem  7953  wdomtr  8090  unxpwdom2  8103  fpwwe2lem13  9066  grur1a  9243  grutsk  9246  fimaxre2  10552  xlesubadd  11549  cshwidxmod  12890  sqreu  13402  pcxcl  14773  pcmpt  14800  symggen  17062  isabvd  17983  lspprat  18311  mdetralt  19564  ordtrest2lem  20150  ordthauslem  20330  comppfsc  20478  fbssint  20784  fclscf  20971  tgptsmscld  21096  ovoliunnul  22338  itg11  22526  i1fadd  22530  fta1g  22993  plydiveu  23119  fta1  23129  mulcxp  23495  cxpsqrt  23513  ostth3  24339  brbtwn2  24781  colinearalg  24786  clwwisshclww  25380  ordtrest2NEWlem  28567  subfacp1lem5  29695  frmin  30267  btwnexch2  30575  fnemeet2  30808  fnejoin2  30810  limsucncmpi  30890  areacirc  31740  sstotbnd2  31809  ssbnd  31823  prdsbnd2  31830  rrncmslem  31867  atnlt  32587  atlelt  32711  llnnlt  32796  lplnnlt  32838  lvolnltN  32891  pmapglb2N  33044  pmapglb2xN  33045  paddasslem14  33106  cdleme27a  33642  iccpartigtl  38126
  Copyright terms: Public domain W3C validator