Theorem necon2bi 2689

Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)

Hypothesis

Ref	Expression
necon2bi.1	|- ( ph -> A =/= B )

Assertion

Ref	Expression
necon2bi	|- ( A = B -> -. ph )

Proof of Theorem necon2bi

Step	Hyp	Ref	Expression
1		necon2bi.1	. . 3 |- ( ph -> A =/= B )
2	1	neneqd 2655	. 2 |- ( ph -> -. A = B )
3	2	con2i 120	1 |- ( A = B -> -. ph )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1370   =/= wne 2648

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 2650

This theorem is referenced by:  necon4iOLD  2697  minel  3843  rzal  3890  difsnb  4124  reusv7OLD  4613  dtrucor2  4635  kmlem6  8436  winainflem  8972  0npi  9163  0npr  9273  0nsr  9358  renfdisj  9549  1div0  10107  rexmul  11346  rennim  12847  mrissmrcd  14698  prmirred  18045  prmirredOLD  18048  pthaus  19344  rplogsumlem2  22868  pntrlog2bndlem4  22963  pntrlog2bndlem5  22964  1div0apr  23814  subfacp1lem6  27218  itg2addnclem3  28594  sdrgacs  29707  rzalf  29888  bnj1311  32348  bj-dtrucor2v  32655  cdleme31id  34377