Theorem necon3bd 2407

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

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

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 2365

This theorem is referenced by:  nelne1  2454  nelne2  2455  nssne1  3237  nssne2  3238  disjne  3500  difsn  3755  nbrne1  4048  nbrne2  4049  ac6sfi  6954  indpi  7402  zneo  9418  pc2dvds  12468  pcadd  12478  oddprmdvds  12492  4sqlem11  12539  isnzr2  13680  lssvneln0  13869  lgsne0  15154