Theorem necon2bi 2694

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   =/= wne 2652

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 2654

This theorem is referenced by:  necon4iOLD  2702  minel  3885  rzal  3934  difsnb  4174  reusv7OLD  4668  dtrucor2  4690  kmlem6  8552  winainflem  9088  0npi  9277  0npr  9387  0nsr  9473  1div0  10229  rexmul  11488  rennim  13083  mrissmrcd  15056  prmirred  18651  prmirredOLD  18654  pthaus  20264  rplogsumlem2  23795  pntrlog2bndlem4  23890  pntrlog2bndlem5  23891  1div0apr  25302  subfacp1lem6  28804  itg2addnclem3  30230  sdrgacs  31312  rzalf  31553  jumpncnp  31862  fourierswlem  32174  bnj1311  34181  bj-dtrucor2v  34488  cdleme31id  36221