Theorem necon3bd 2446

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2403

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 2404

This theorem is referenced by:  nelne1  2493  nelne2  2494  nssne1  3286  nssne2  3287  disjne  3550  difsn  3815  nbrne1  4112  nbrne2  4113  ac6sfi  7130  indpi  7622  zneo  9642  pc2dvds  12983  pcadd  12993  oddprmdvds  13007  4sqlem11  13054  isnzr2  14279  lssvneln0  14469  pellexlem1  15791  lgsne0  15857  lgsquadlem2  15897  lgsquadlem3  15898