Theorem necon2bi 2824

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 2799	. 2 |- ( ph -> -. A = B )
3	2	con2i 134	1 |- ( A = B -> -. ph )

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:  minelOLD  4034  rzal  4073  difsnb  4337  dtrucor2  4901  kmlem6  8977  winainflem  9515  0npi  9704  0npr  9814  0nsr  9900  1div0  10686  rexmul  12101  rennim  13979  mrissmrcd  16300  prmirred  19843  pthaus  21441  rplogsumlem2  25174  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  numclwwlkffin0  27215  1div0apr  27324  bnj1311  31092  subfacp1lem6  31167  bj-dtrucor2v  32801  itg2addnclem3  33463  cdleme31id  35682  sdrgacs  37771  rzalf  39176  jumpncnp  40111  fourierswlem  40447