Theorem necon2ad 2471

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

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

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 2415

This theorem is referenced by:  necon2d  2473  prneimg  3883  tz7.2  4480  nordeq  4671  pr2ne  7502  ltne  8374  apne  8914  xrltne  10165  npnflt  10167  nmnfgt  10170  ge0nemnf  10176  rpexp  12875  sqrt2irr  12884  pcgcd1  13051  nzrunit  14433  lgsmod  16025