Theorem necon3bd 2410

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1364   =/= wne 2367

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 615  ax-in2 616

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

This theorem is referenced by:  nelne1  2457  nelne2  2458  nssne1  3241  nssne2  3242  disjne  3504  difsn  3759  nbrne1  4052  nbrne2  4053  ac6sfi  6959  indpi  7409  zneo  9427  pc2dvds  12499  pcadd  12509  oddprmdvds  12523  4sqlem11  12570  isnzr2  13740  lssvneln0  13929  lgsne0  15279  lgsquadlem2  15319  lgsquadlem3  15320