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 ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

This proof depends on 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 proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  necon2d  2479  prneimg  3899  tz7.2  4499  nordeq  4691  pr2ne  7538  ltne  8410  apne  8953  xrltne  10225  npnflt  10227  nmnfgt  10230  ge0nemnf  10236  rpexp  12948  sqrt2irr  12957  pcgcd1  13127  nzrunit  14544  lgsmod  16243