Theorem necon1bd 2661

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 2640	. . 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 1383   =/= wne 2638

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 2640

This theorem is referenced by:  necon4ad  2663  suppssrOLD  6006  fvclss  6139  suppssr  6933  eceqoveq  7418  fofinf1o  7803  cantnfp1lem3  8102  cantnfp1  8103  cantnfp1lem3OLD  8128  cantnfp1OLD  8129  mul0or  10195  inelr  10532  rimul  10533  rlimuni  13352  pc2dvds  14279  divsfval  14821  pleval2i  15468  lssvs0or  17630  lspsnat  17665  lmmo  19754  filssufilg  20285  hausflimi  20354  fclscf  20399  xrsmopn  21190  rectbntr0  21210  bcth3  21643  limcco  22170  ig1pdvds  22450  plyco0  22462  plypf1  22482  coeeulem  22494  coeidlem  22507  coeid3  22510  coemullem  22519  coemulhi  22523  coemulc  22524  dgradd2  22537  vieta1lem2  22579  dvtaylp  22637  musum  23339  perfectlem2  23377  dchrelbas3  23385  dchrmulid2  23399  dchreq  23405  dchrsum  23416  dchrisum0re  23570  coltr  23899  lmieu  24022  elspansn5  26364  atomli  27173  onsucconi  29877  congabseq  30887  lshpcmp  34453  lsator0sp  34466  atnle  34782  atlatmstc  34784  osumcllem8N  35427  osumcllem11N  35430  pexmidlem5N  35438  pexmidlem8N  35441  dochsat0  36924  dochexmidlem5  36931  dochexmidlem8  36934