Theorem necon1bd 2812

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon4ad  2813  fvclss  6500  suppssr  7326  eceqoveq  7853  fofinf1o  8241  cantnfp1lem3  8577  cantnfp1  8578  mul0or  10667  inelr  11010  rimul  11011  rlimuni  14281  pc2dvds  15583  divsfval  16207  pleval2i  16964  lssvs0or  19110  lspsnat  19145  lmmo  21184  filssufilg  21715  hausflimi  21784  fclscf  21829  xrsmopn  22615  rectbntr0  22635  bcth3  23128  limcco  23657  ig1pdvds  23936  plyco0  23948  plypf1  23968  coeeulem  23980  coeidlem  23993  coeid3  23996  coemullem  24006  coemulhi  24010  coemulc  24011  dgradd2  24024  vieta1lem2  24066  dvtaylp  24124  musum  24917  perfectlem2  24955  dchrelbas3  24963  dchrmulid2  24977  dchreq  24983  dchrsum  24994  gausslemma2dlem4  25094  dchrisum0re  25202  coltr  25542  lmieu  25676  elspansn5  28433  atomli  29241  onsucconni  32436  poimirlem8  33417  poimirlem9  33418  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem26  33435  lshpcmp  34275  lsator0sp  34288  atnle  34604  atlatmstc  34606  osumcllem8N  35249  osumcllem11N  35252  pexmidlem5N  35260  pexmidlem8N  35263  dochsat0  36746  dochexmidlem5  36753  dochexmidlem8  36756  congabseq  37541  perfectALTVlem2  41631