Theorem necon2ad 2432

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1372   =/= wne 2375

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 2376

This theorem is referenced by:  necon2d  2434  prneimg  3814  tz7.2  4400  nordeq  4591  pr2ne  7299  ltne  8156  apne  8695  xrltne  9934  npnflt  9936  nmnfgt  9939  ge0nemnf  9945  rpexp  12417  sqrt2irr  12426  pcgcd1  12593  nzrunit  13892  lgsmod  15445