Theorem necon1bd 2635

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

Step	Hyp	Ref	Expression
1		necon1bd.1	. . 3 |- ( ph -> ( A =/= B -> ps ) )
2	1	con3d 127	. 2 |- ( ph -> ( -. ps -> -. A =/= B ) )
3		nne 2571	. 2 |- ( -. A =/= B <-> A = B )
4	2, 3	syl6ib 218	1 |- ( ph -> ( -. ps -> A = B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1649   =/= wne 2567

This theorem is referenced by:  suppssr  5823  fvclss  5939  eceqoveq  6968  fofinf1o  7346  cantnfp1lem3  7592  cantnfp1  7593  mul0or  9618  inelr  9946  rimul  9947  rlimuni  12299  pc2dvds  13207  divsfval  13727  pleval2i  14376  lssvs0or  16137  lspsnat  16172  lmmo  17398  filssufilg  17896  hausflimi  17965  fclscf  18010  xrsmopn  18796  rectbntr0  18816  bcth3  19237  limcco  19733  ig1pdvds  20052  plyco0  20064  plypf1  20084  coeeulem  20096  coeidlem  20109  coeid3  20112  coemullem  20121  coemulhi  20125  coemulc  20126  dgradd2  20139  vieta1lem2  20181  dvtaylp  20239  musum  20929  perfectlem2  20967  dchrelbas3  20975  dchrmulid2  20989  dchreq  20995  dchrsum  21006  dchrisum0re  21160  elspansn5  23029  atomli  23838  onsucconi  26091  congabseq  26929  lshpcmp  29471  lsator0sp  29484  atnle  29800  atlatmstc  29802  osumcllem8N  30445  osumcllem11N  30448  pexmidlem5N  30456  pexmidlem8N  30459  dochsat0  31940  dochexmidlem5  31947  dochexmidlem8  31950

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 2569