Theorem necon2bi 2661

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1437   =/= wne 2618

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 188  df-ne 2620

This theorem is referenced by:  necon4iOLD  2669  minel  3848  rzal  3899  difsnb  4139  dtrucor2  4652  kmlem6  8586  winainflem  9119  0npi  9308  0npr  9418  0nsr  9504  1div0  10272  rexmul  11558  rennim  13291  mrissmrcd  15534  prmirred  19053  pthaus  20640  rplogsumlem2  24310  pntrlog2bndlem4  24405  pntrlog2bndlem5  24406  1div0apr  25891  bnj1311  29829  subfacp1lem6  29904  bj-dtrucor2v  31374  itg2addnclem3  31909  cdleme31id  33880  sdrgacs  35987  rzalf  37199  jumpncnp  37596  fourierswlem  37914