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

Theorem necon1bd 2618
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 127 . 2  |-  ( ph  ->  ( -.  ps  ->  -.  A  =/=  B ) )
3 nne 2554 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 218 1  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2550
This theorem is referenced by:  suppssr  5803  fvclss  5919  eceqoveq  6945  fofinf1o  7323  cantnfp1lem3  7569  cantnfp1  7570  mul0or  9594  inelr  9922  rimul  9923  rlimuni  12271  pc2dvds  13179  divsfval  13699  pleval2i  14348  lssvs0or  16109  lspsnat  16144  lmmo  17366  filssufilg  17864  hausflimi  17933  fclscf  17978  xrsmopn  18714  rectbntr0  18734  bcth3  19153  limcco  19647  ig1pdvds  19966  plyco0  19978  plypf1  19998  coeeulem  20010  coeidlem  20023  coeid3  20026  coemullem  20035  coemulhi  20039  coemulc  20040  dgradd2  20053  vieta1lem2  20095  dvtaylp  20153  musum  20843  perfectlem2  20881  dchrelbas3  20889  dchrmulid2  20903  dchreq  20909  dchrsum  20920  dchrisum0re  21074  elspansn5  22924  atomli  23733  onsucconi  25901  congabseq  26730  lshpcmp  29103  lsator0sp  29116  atnle  29432  atlatmstc  29434  osumcllem8N  30077  osumcllem11N  30080  pexmidlem5N  30088  pexmidlem8N  30091  dochsat0  31572  dochexmidlem5  31579  dochexmidlem8  31582
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 178  df-ne 2552
  Copyright terms: Public domain W3C validator