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

Theorem necon1bd 2527
Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon1bd.1  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
Assertion
Ref Expression
necon1bd  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )

Proof of Theorem necon1bd
StepHypRef Expression
1 necon1bd.1 . . 3  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
21con3d 125 . 2  |-  ( ph  ->  ( -.  ps  ->  -.  A  =/=  B ) )
3 nne 2463 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 217 1  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  suppssr  5675  fvclss  5776  eceqoveq  6779  fofinf1o  7153  cantnfp1lem3  7398  cantnfp1  7399  mul0or  9424  inelr  9752  rimul  9753  rlimuni  12040  pc2dvds  12947  divsfval  13465  pleval2i  14114  lssvs0or  15879  lspsnat  15914  lmmo  17124  filssufilg  17622  hausflimi  17691  fclscf  17736  xrsmopn  18334  rectbntr0  18353  bcth3  18769  limcco  19259  ig1pdvds  19578  plyco0  19590  plypf1  19610  coeeulem  19622  coeidlem  19635  coeid3  19638  coemullem  19647  coemulhi  19651  coemulc  19652  dgradd2  19665  vieta1lem2  19707  dvtaylp  19765  musum  20447  perfectlem2  20485  dchrelbas3  20493  dchrmulid2  20507  dchreq  20513  dchrsum  20524  dchrisum0re  20678  elspansn5  22169  atomli  22978  onsucconi  24948  congabseq  27164  lshpcmp  29800  lsator0sp  29813  atnle  30129  atlatmstc  30131  osumcllem8N  30774  osumcllem11N  30777  pexmidlem5N  30785  pexmidlem8N  30788  dochsat0  32269  dochexmidlem5  32276  dochexmidlem8  32279
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 2461
  Copyright terms: Public domain W3C validator