Theorem necon1bd 2674

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 133	. 2 |- ( ph -> ( -. ps -> -. A =/= B ) )
3		nne 2607	. 2 |- ( -. A =/= B <-> A = B )
4	2, 3	syl6ib 226	1 |- ( ph -> ( -. ps -> A = B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1369   =/= wne 2601

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 185  df-ne 2603

This theorem is referenced by:  suppssrOLD  5832  fvclss  5954  suppssr  6715  eceqoveq  7197  fofinf1o  7584  cantnfp1lem3  7880  cantnfp1  7881  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  mul0or  9968  inelr  10304  rimul  10305  rlimuni  13020  pc2dvds  13937  divsfval  14477  pleval2i  15126  lssvs0or  17171  lspsnat  17206  lmmo  18964  filssufilg  19464  hausflimi  19533  fclscf  19578  xrsmopn  20369  rectbntr0  20389  bcth3  20822  limcco  21348  ig1pdvds  21628  plyco0  21640  plypf1  21660  coeeulem  21672  coeidlem  21685  coeid3  21688  coemullem  21697  coemulhi  21701  coemulc  21702  dgradd2  21715  vieta1lem2  21757  dvtaylp  21815  musum  22511  perfectlem2  22549  dchrelbas3  22557  dchrmulid2  22571  dchreq  22577  dchrsum  22588  dchrisum0re  22742  elspansn5  24945  atomli  25754  onsucconi  28253  congabseq  29288  lshpcmp  32526  lsator0sp  32539  atnle  32855  atlatmstc  32857  osumcllem8N  33500  osumcllem11N  33503  pexmidlem5N  33511  pexmidlem8N  33514  dochsat0  34995  dochexmidlem5  35002  dochexmidlem8  35005