Theorem necon2ad 2421

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1364   =/= wne 2364

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 2365

This theorem is referenced by:  necon2d  2423  prneimg  3801  tz7.2  4386  nordeq  4577  pr2ne  7254  ltne  8106  apne  8644  xrltne  9882  npnflt  9884  nmnfgt  9887  ge0nemnf  9893  rpexp  12294  sqrt2irr  12303  pcgcd1  12469  nzrunit  13687  lgsmod  15183