Theorem necon2bd 2682

Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)

Hypothesis

Ref	Expression
necon2bd.1	|- ( ph -> ( ps -> A =/= B ) )

Assertion

Ref	Expression
necon2bd	|- ( ph -> ( A = B -> -. ps ) )

Proof of Theorem necon2bd

Step	Hyp	Ref	Expression
1		necon2bd.1	. . 3 |- ( ph -> ( ps -> A =/= B ) )
2		df-ne 2664	. . 3 |- ( A =/= B <-> -. A = B )
3	1, 2	syl6ib 226	. 2 |- ( ph -> ( ps -> -. A = B ) )
4	3	con2d 115	1 |- ( ph -> ( A = B -> -. ps ) )

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:  necon4bd  2689  necon4d  2694  disjiun  4443  eceqoveq  7428  en3lp  8045  infpssrlem5  8699  nneo  10956  zeo2  10959  sqrt2irr  13860  coprm  14117  dfphi2  14180  pltirr  15467  oddvdsnn0  16441  psgnodpmr  18495  supnfcls  20389  flimfnfcls  20397  metds0  21222  metdseq0  21226  metnrmlem1a  21230  sineq0  22780  lgsqr  23487  staddi  26979  stadd3i  26981  eulerpartlems  28115  erdszelem8  28458  ordcmp  29830  finminlem  30054  bezoutr1  30843  cvrnrefN  34435  trlnidatb  35329