Theorem necon2bd 2646

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 2627	. . 3 |- ( A =/= B <-> -. A = B )
3	1, 2	syl6ib 229	. 2 |- ( ph -> ( ps -> -. A = B ) )
4	3	con2d 118	1 |- ( ph -> ( A = B -> -. ps ) )

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

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 2627

This theorem is referenced by:  necon4bd  2653  necon4d  2658  disjiun  4417  eceqoveq  7476  en3lp  8121  infpssrlem5  8735  nneo  11019  zeo2  11022  sqrt2irr  14279  coprm  14628  dfphi2  14691  pltirr  16160  oddvdsnn0  17135  psgnodpmr  19089  supnfcls  20966  flimfnfcls  20974  metds0  21778  metdseq0  21782  metnrmlem1a  21786  sineq0  23341  lgsqr  24137  staddi  27734  stadd3i  27736  eulerpartlems  29019  erdszelem8  29709  finminlem  30759  ordcmp  30892  poimirlem18  31662  poimirlem21  31665  cvrnrefN  32557  trlnidatb  33452  bezoutr1  35542