Theorem necon2ad 2434

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

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

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 2378

This theorem is referenced by:  necon2d  2436  prneimg  3821  tz7.2  4409  nordeq  4600  pr2ne  7315  ltne  8177  apne  8716  xrltne  9955  npnflt  9957  nmnfgt  9960  ge0nemnf  9966  rpexp  12550  sqrt2irr  12559  pcgcd1  12726  nzrunit  14025  lgsmod  15578