Theorem necon2bd 2664

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 2647	. . 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 1370   =/= wne 2645

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 2647

This theorem is referenced by:  necon4bd  2671  necon4d  2676  disjiun  4385  eceqoveq  7310  en3lp  7928  infpssrlem5  8582  nneo  10831  zeo2  10834  sqr2irr  13644  coprm  13899  dfphi2  13962  pltirr  15247  oddvdsnn0  16163  psgnodpmr  18140  supnfcls  19720  flimfnfcls  19728  metds0  20553  metdseq0  20557  metnrmlem1a  20561  sineq0  22111  lgsqr  22813  staddi  25797  stadd3i  25799  eulerpartlems  26882  erdszelem8  27225  ordcmp  28432  finminlem  28656  bezoutr1  29472  cvrnrefN  33246  trlnidatb  34140