Theorem necon3bd 2421

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1373   =/= wne 2378

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 2379

This theorem is referenced by:  nelne1  2468  nelne2  2469  nssne1  3259  nssne2  3260  disjne  3522  difsn  3781  nbrne1  4078  nbrne2  4079  ac6sfi  7021  indpi  7490  zneo  9509  pc2dvds  12768  pcadd  12778  oddprmdvds  12792  4sqlem11  12839  isnzr2  14061  lssvneln0  14250  lgsne0  15630  lgsquadlem2  15670  lgsquadlem3  15671