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

Theorem pm2.61dne 2737
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 2620 . . 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 2614
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 2616
This theorem is referenced by:  pm2.61dane  2738  wefrc  4847  wereu2  4850  oe0lem  7226  fisupg  7828  marypha1lem  7956  fiinfg  8024  wdomtr  8099  unxpwdom2  8112  fpwwe2lem13  9074  grur1a  9251  grutsk  9254  fimaxre2  10559  xlesubadd  11556  cshwidxmod  12907  sqreu  13423  pcxcl  14809  pcmpt  14836  symggen  17110  isabvd  18047  lspprat  18375  mdetralt  19631  ordtrest2lem  20217  ordthauslem  20397  comppfsc  20545  fbssint  20851  fclscf  21038  tgptsmscld  21163  ovoliunnul  22458  itg11  22647  i1fadd  22651  fta1g  23116  plydiveu  23249  fta1  23259  mulcxp  23628  cxpsqrt  23646  ostth3  24474  brbtwn2  24933  colinearalg  24938  clwwisshclww  25533  ordtrest2NEWlem  28736  subfacp1lem5  29915  frmin  30487  btwnexch2  30795  fnemeet2  31028  fnejoin2  31030  limsucncmpi  31110  areacirc  32001  sstotbnd2  32070  ssbnd  32084  prdsbnd2  32091  rrncmslem  32128  atnlt  32848  atlelt  32972  llnnlt  33057  lplnnlt  33099  lvolnltN  33152  pmapglb2N  33305  pmapglb2xN  33306  paddasslem14  33367  cdleme27a  33903  iccpartigtl  38607
  Copyright terms: Public domain W3C validator