Theorem necon2bi 2665

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1454   =/= wne 2632

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 190  df-ne 2634

This theorem is referenced by:  minel  3831  rzal  3882  difsnb  4126  dtrucor2  4647  kmlem6  8610  winainflem  9143  0npi  9332  0npr  9442  0nsr  9528  1div0  10298  rexmul  11585  rennim  13350  mrissmrcd  15594  prmirred  19114  pthaus  20701  rplogsumlem2  24371  pntrlog2bndlem4  24466  pntrlog2bndlem5  24467  1div0apr  25953  bnj1311  29881  subfacp1lem6  29956  bj-dtrucor2v  31460  itg2addnclem3  32039  cdleme31id  34005  sdrgacs  36111  rzalf  37377  jumpncnp  37813  fourierswlem  38131