Theorem necon1bd 2669

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1362   =/= wne 2596

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 2598

This theorem is referenced by:  suppssrOLD  5825  fvclss  5946  suppssr  6709  eceqoveq  7193  fofinf1o  7580  cantnfp1lem3  7876  cantnfp1  7877  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  mul0or  9964  inelr  10300  rimul  10301  rlimuni  13012  pc2dvds  13928  divsfval  14468  pleval2i  15117  lssvs0or  17113  lspsnat  17148  lmmo  18826  filssufilg  19326  hausflimi  19395  fclscf  19440  xrsmopn  20231  rectbntr0  20251  bcth3  20684  limcco  21210  ig1pdvds  21533  plyco0  21545  plypf1  21565  coeeulem  21577  coeidlem  21590  coeid3  21593  coemullem  21602  coemulhi  21606  coemulc  21607  dgradd2  21620  vieta1lem2  21662  dvtaylp  21720  musum  22416  perfectlem2  22454  dchrelbas3  22462  dchrmulid2  22476  dchreq  22482  dchrsum  22493  dchrisum0re  22647  elspansn5  24800  atomli  25609  onsucconi  28131  congabseq  29162  lshpcmp  32206  lsator0sp  32219  atnle  32535  atlatmstc  32537  osumcllem8N  33180  osumcllem11N  33183  pexmidlem5N  33191  pexmidlem8N  33194  dochsat0  34675  dochexmidlem5  34682  dochexmidlem8  34685