Theorem necon2bd 2810

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon4bd  2814  necon4d  2818  minel  4033  disjiun  4640  eceqoveq  7853  en3lp  8513  infpssrlem5  9129  nneo  11461  zeo2  11464  sqrt2irr  14979  bezoutr1  15282  coprm  15423  dfphi2  15479  pltirr  16963  oddvdsnn0  17963  psgnodpmr  19936  supnfcls  21824  flimfnfcls  21832  metds0  22653  metdseq0  22657  metnrmlem1a  22661  sineq0  24273  lgsqr  25076  staddi  29105  stadd3i  29107  eulerpartlems  30422  erdszelem8  31180  finminlem  32312  ordcmp  32446  poimirlem18  33427  poimirlem21  33430  cvrnrefN  34569  trlnidatb  35464