Theorem necon1bd 2654

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 2635	. . 3 |- ( A =/= B <-> -. A = B )
2		necon1bd.1	. . 3 |- ( ph -> ( A =/= B -> ps ) )
3	1, 2	syl5bir 226	. 2 |- ( ph -> ( -. A = B -> ps ) )
4	3	con1d 129	1 |- ( ph -> ( -. ps -> A = B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1455   =/= wne 2633

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 190  df-ne 2635

This theorem is referenced by:  necon4ad  2655  fvclss  6172  suppssr  6973  eceqoveq  7494  fofinf1o  7878  cantnfp1lem3  8211  cantnfp1  8212  mul0or  10280  inelr  10627  rimul  10628  rlimuni  13663  pc2dvds  14877  divsfval  15502  pleval2i  16259  lssvs0or  18382  lspsnat  18417  lmmo  20445  filssufilg  20975  hausflimi  21044  fclscf  21089  xrsmopn  21879  rectbntr0  21899  bcth3  22348  limcco  22897  ig1pdvds  23177  ig1pdvdsOLD  23183  plyco0  23195  plypf1  23215  coeeulem  23227  coeidlem  23240  coeid3  23243  coemullem  23253  coemulhi  23257  coemulc  23258  dgradd2  23271  vieta1lem2  23313  dvtaylp  23374  musum  24169  perfectlem2  24207  dchrelbas3  24215  dchrmulid2  24229  dchreq  24235  dchrsum  24246  dchrisum0re  24400  coltr  24741  lmieu  24875  elspansn5  27276  atomli  28084  onsucconi  31146  poimirlem8  31993  poimirlem9  31994  poimirlem18  32003  poimirlem21  32006  poimirlem22  32007  poimirlem26  32011  lshpcmp  32599  lsator0sp  32612  atnle  32928  atlatmstc  32930  osumcllem8N  33573  osumcllem11N  33576  pexmidlem5N  33584  pexmidlem8N  33587  dochsat0  35070  dochexmidlem5  35077  dochexmidlem8  35080  congabseq  35869  perfectALTVlem2  38882