Theorem necon3bd 2419

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

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

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 2377

This theorem is referenced by:  nelne1  2466  nelne2  2467  nssne1  3251  nssne2  3252  disjne  3514  difsn  3770  nbrne1  4063  nbrne2  4064  ac6sfi  6995  indpi  7455  zneo  9474  pc2dvds  12653  pcadd  12663  oddprmdvds  12677  4sqlem11  12724  isnzr2  13946  lssvneln0  14135  lgsne0  15515  lgsquadlem2  15555  lgsquadlem3  15556