Theorem necon2bi 2704

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1379   =/= wne 2662

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 2664

This theorem is referenced by:  necon4iOLD  2712  minel  3882  rzal  3929  difsnb  4169  reusv7OLD  4659  dtrucor2  4681  kmlem6  8531  winainflem  9067  0npi  9256  0npr  9366  0nsr  9452  renfdisj  9643  1div0  10204  rexmul  11459  rennim  13029  mrissmrcd  14888  prmirred  18289  prmirredOLD  18292  pthaus  19871  rplogsumlem2  23395  pntrlog2bndlem4  23490  pntrlog2bndlem5  23491  1div0apr  24849  subfacp1lem6  28266  itg2addnclem3  29643  sdrgacs  30755  rzalf  30970  jumpncnp  31237  fourierswlem  31531  bnj1311  33159  bj-dtrucor2v  33468  cdleme31id  35190