Theorem necon3bd 2455

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 636	. 2 |- ( ph -> ( -. ps -> -. A = B ) )
3		df-ne 2413	. 2 |- ( A =/= B <-> -. A = B )
4	2, 3	imbitrrdi 162	1 |- ( ph -> ( -. ps -> A =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2412

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 619  ax-in2 620

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

This theorem is referenced by:  nelne1  2502  nelne2  2503  nssne1  3296  nssne2  3297  disjne  3562  difsn  3831  nbrne1  4128  nbrne2  4129  ac6sfi  7155  indpi  7657  zneo  9679  pc2dvds  13028  pcadd  13038  oddprmdvds  13052  4sqlem11  13099  isnzr2  14329  lssvneln0  14521  pellexlem1  15845  lgsne0  15911  lgsquadlem2  15951  lgsquadlem3  15952