Theorem necon2bbid 2837

Description: Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)

Hypothesis

Ref	Expression
necon2bbid.1	|- ( ph -> ( ps <-> A =/= B ) )

Assertion

Ref	Expression
necon2bbid	|- ( ph -> ( A = B <-> -. ps ) )

Proof of Theorem necon2bbid

Step	Hyp	Ref	Expression
1		notnotb 304	. . 3 |- ( ps <-> -. -. ps )
2		necon2bbid.1	. . 3 |- ( ph -> ( ps <-> A =/= B ) )
3	1, 2	syl5rbbr 275	. 2 |- ( ph -> ( A =/= B <-> -. -. ps ) )
4	3	necon4abid 2834	1 |- ( ph -> ( A = B <-> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   = 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:  necon4bid  2839  omwordi  7651  omass  7660  nnmwordi  7715  sdom1  8160  pceq0  15575  f1otrspeq  17867  pmtrfinv  17881  symggen  17890  psgnunilem1  17913  mdetralt  20414  mdetunilem7  20424  ftalem5  24803  fsumvma  24938  dchrelbas4  24968  fsumcvg4  29996  nosepssdm  31836  lkreqN  34457