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  4399  nordeq  4590  pr2ne  7282  ltne  8139  apne  8678  xrltne  9917  npnflt  9919  nmnfgt  9922  ge0nemnf  9928  rpexp  12394  sqrt2irr  12403  pcgcd1  12570  nzrunit  13868  lgsmod  15421