Theorem necon2ad 2469

Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)

Hypothesis

Ref	Expression
necon2ad.1	|- ( ph -> ( A = B -> -. ps ) )

Assertion

Ref	Expression
necon2ad	|- ( ph -> ( ps -> A =/= B ) )

Proof of Theorem necon2ad

Step	Hyp	Ref	Expression
1		necon2ad.1	. . 3 |- ( ph -> ( A = B -> -. ps ) )
2	1	con2d 629	. 2 |- ( ph -> ( ps -> -. A = B ) )
3		df-ne 2413	. 2 |- ( A =/= B <-> -. A = B )
4	2, 3	imbitrrdi 162	1 |- ( ph -> ( ps -> A =/= B ) )

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

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 2413

This theorem is referenced by:  necon2d  2471  prneimg  3878  tz7.2  4475  nordeq  4666  pr2ne  7489  ltne  8358  apne  8897  xrltne  10146  npnflt  10148  nmnfgt  10151  ge0nemnf  10157  rpexp  12850  sqrt2irr  12859  pcgcd1  13026  nzrunit  14333  lgsmod  15899