Theorem necon1bd 2600

Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

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		df-ne 2579	. . 3 |- ( A =/= B <-> -. A = B )
2		necon1bd.1	. . 3 |- ( ph -> ( A =/= B -> ps ) )
3	1, 2	syl5bir 218	. 2 |- ( ph -> ( -. A = B -> ps ) )
4	3	con1d 124	1 |- ( ph -> ( -. ps -> A = B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1399   =/= wne 2577

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 2579

This theorem is referenced by:  necon4ad  2602  suppssrOLD  5923  fvclss  6055  suppssr  6849  eceqoveq  7334  fofinf1o  7716  cantnfp1lem3  8012  cantnfp1  8013  cantnfp1lem3OLD  8038  cantnfp1OLD  8039  mul0or  10106  inelr  10442  rimul  10443  rlimuni  13375  pc2dvds  14404  divsfval  14954  pleval2i  15711  lssvs0or  17869  lspsnat  17904  lmmo  19967  filssufilg  20497  hausflimi  20566  fclscf  20611  xrsmopn  21402  rectbntr0  21422  bcth3  21855  limcco  22382  ig1pdvds  22662  plyco0  22674  plypf1  22694  coeeulem  22706  coeidlem  22719  coeid3  22722  coemullem  22732  coemulhi  22736  coemulc  22737  dgradd2  22750  vieta1lem2  22792  dvtaylp  22850  musum  23584  perfectlem2  23622  dchrelbas3  23630  dchrmulid2  23644  dchreq  23650  dchrsum  23661  dchrisum0re  23815  coltr  24147  lmieu  24270  elspansn5  26609  atomli  27417  onsucconi  30055  congabseq  31077  perfectALTVlem2  32544  lshpcmp  35126  lsator0sp  35139  atnle  35455  atlatmstc  35457  osumcllem8N  36100  osumcllem11N  36103  pexmidlem5N  36111  pexmidlem8N  36114  dochsat0  37597  dochexmidlem5  37604  dochexmidlem8  37607