Theorem necon2ad 2477

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

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 623  ax-in2 624

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

This theorem is referenced by:  necon2d  2479  prneimg  3894  tz7.2  4494  nordeq  4686  pr2ne  7528  ltne  8400  apne  8941  xrltne  10194  npnflt  10196  nmnfgt  10199  ge0nemnf  10205  rpexp  12909  sqrt2irr  12918  pcgcd1  13085  nzrunit  14468  lgsmod  16059