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

Theorem necon1bd 2514
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 2450 . 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 1623    =/= wne 2446
This theorem is referenced by:  suppssr  5659  fvclss  5760  eceqoveq  6763  fofinf1o  7137  cantnfp1lem3  7382  cantnfp1  7383  mul0or  9408  inelr  9736  rimul  9737  rlimuni  12024  pc2dvds  12931  divsfval  13449  pleval2i  14098  lssvs0or  15863  lspsnat  15898  lmmo  17108  filssufilg  17606  hausflimi  17675  fclscf  17720  xrsmopn  18318  rectbntr0  18337  bcth3  18753  limcco  19243  ig1pdvds  19562  plyco0  19574  plypf1  19594  coeeulem  19606  coeidlem  19619  coeid3  19622  coemullem  19631  coemulhi  19635  coemulc  19636  dgradd2  19649  vieta1lem2  19691  dvtaylp  19749  musum  20431  perfectlem2  20469  dchrelbas3  20477  dchrmulid2  20491  dchreq  20497  dchrsum  20508  dchrisum0re  20662  elspansn5  22153  atomli  22962  onsucconi  24876  congabseq  27061  lshpcmp  29178  lsator0sp  29191  atnle  29507  atlatmstc  29509  osumcllem8N  30152  osumcllem11N  30155  pexmidlem5N  30163  pexmidlem8N  30166  dochsat0  31647  dochexmidlem5  31654  dochexmidlem8  31657
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 2448
  Copyright terms: Public domain W3C validator