Theorem necon1bd 2678

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 2657	. . 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 1374   =/= wne 2655

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 2657

This theorem is referenced by:  necon4ad  2680  suppssrOLD  6006  fvclss  6133  suppssr  6921  eceqoveq  7406  fofinf1o  7790  cantnfp1lem3  8088  cantnfp1  8089  cantnfp1lem3OLD  8114  cantnfp1OLD  8115  mul0or  10178  inelr  10515  rimul  10516  rlimuni  13322  pc2dvds  14250  divsfval  14791  pleval2i  15440  lssvs0or  17532  lspsnat  17567  lmmo  19640  filssufilg  20140  hausflimi  20209  fclscf  20254  xrsmopn  21045  rectbntr0  21065  bcth3  21498  limcco  22025  ig1pdvds  22305  plyco0  22317  plypf1  22337  coeeulem  22349  coeidlem  22362  coeid3  22365  coemullem  22374  coemulhi  22378  coemulc  22379  dgradd2  22392  vieta1lem2  22434  dvtaylp  22492  musum  23188  perfectlem2  23226  dchrelbas3  23234  dchrmulid2  23248  dchreq  23254  dchrsum  23265  dchrisum0re  23419  coltr  23733  lmieu  23820  elspansn5  26154  atomli  26963  onsucconi  29465  congabseq  30503  lshpcmp  33660  lsator0sp  33673  atnle  33989  atlatmstc  33991  osumcllem8N  34634  osumcllem11N  34637  pexmidlem5N  34645  pexmidlem8N  34648  dochsat0  36129  dochexmidlem5  36136  dochexmidlem8  36139