Theorem necon2ad 2404

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1353   =/= wne 2347

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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117  df-ne 2348

This theorem is referenced by:  necon2d  2406  prneimg  3776  tz7.2  4356  nordeq  4545  pr2ne  7193  ltne  8044  apne  8582  xrltne  9815  npnflt  9817  nmnfgt  9820  ge0nemnf  9826  rpexp  12155  sqrt2irr  12164  pcgcd1  12329  nzrunit  13334  lgsmod  14512