Theorem necon3bd 2445

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1397   =/= wne 2402

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 2403

This theorem is referenced by:  nelne1  2492  nelne2  2493  nssne1  3285  nssne2  3286  disjne  3548  difsn  3810  nbrne1  4107  nbrne2  4108  ac6sfi  7086  indpi  7561  zneo  9580  pc2dvds  12902  pcadd  12912  oddprmdvds  12926  4sqlem11  12973  isnzr2  14197  lssvneln0  14386  lgsne0  15766  lgsquadlem2  15806  lgsquadlem3  15807