Theorem necon2bd 2639

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1443   =/= wne 2621

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 189  df-ne 2623

This theorem is referenced by:  necon4bd  2643  necon4d  2647  disjiun  4392  eceqoveq  7465  en3lp  8118  infpssrlem5  8734  nneo  11016  zeo2  11019  sqrt2irr  14294  coprm  14650  dfphi2  14715  pltirr  16202  oddvdsnn0  17186  psgnodpmr  19151  supnfcls  21028  flimfnfcls  21036  metds0  21860  metdseq0  21864  metnrmlem1a  21868  metds0OLD  21875  metdseq0OLD  21879  metnrmlem1aOLD  21883  sineq0  23469  lgsqr  24267  staddi  27892  stadd3i  27894  eulerpartlems  29186  erdszelem8  29914  finminlem  30967  ordcmp  31100  poimirlem18  31951  poimirlem21  31954  cvrnrefN  32842  trlnidatb  33737  bezoutr1  35830