Theorem necon3bd 2463

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)

Hypothesis

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

Assertion

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

Proof of Theorem necon3bd

Step	Hyp	Ref	Expression
1		necon3bd.1	. . 3 |- ( ph -> ( A = B -> ps ) )
2	1	con3d 640	. 2 |- ( ph -> ( -. ps -> -. A = B ) )
3		df-ne 2421	. 2 |- ( A =/= B <-> -. A = B )
4	2, 3	imbitrrdi 162	1 |- ( ph -> ( -. ps -> A =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem depends on definitions:  df-bi 117  df-ne 2421

This theorem is referenced by:  nelne1  2510  nelne2  2511  nssne1  3306  nssne2  3307  disjne  3577  difsn  3847  nbrne1  4144  nbrne2  4145  ac6sfi  7192  indpi  7699  zneo  9726  pc2dvds  13087  pcadd  13097  oddprmdvds  13111  4sqlem11  13158  isnzr2  14464  lssvneln0  14682  pellexlem1  16005  lgsne0  16071  lgsquadlem2  16111  lgsquadlem3  16112