Theorem necon2ad 2809

Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

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		notnot 136	. 2 |- ( ps -> -. -. ps )
2		necon2ad.1	. . 3 |- ( ph -> ( A = B -> -. ps ) )
3	2	necon3bd 2808	. 2 |- ( ph -> ( -. -. ps -> A =/= B ) )
4	1, 3	syl5 34	1 |- ( ph -> ( ps -> A =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-ne 2795

This theorem is referenced by:  necon2d  2817  prneimg  4388  tz7.2  5098  nordeq  5742  omxpenlem  8061  pr2ne  8828  cflim2  9085  cfslb2n  9090  ltne  10134  sqrt2irr  14979  rpexp  15432  pcgcd1  15581  plttr  16970  odhash3  17991  lbspss  19082  nzrunit  19267  en2top  20789  fbfinnfr  21645  ufileu  21723  alexsubALTlem4  21854  lebnumlem1  22760  lebnumlem2  22761  lebnumlem3  22762  ivthlem2  23221  ivthlem3  23222  dvne0  23774  deg1nn0clb  23850  lgsmod  25048  axlowdimlem16  25837  upgrewlkle2  26502  wlkon2n0  26562  pthdivtx  26625  normgt0  27984  nodenselem4  31837  nodenselem5  31838  nodenselem7  31840  slerec  31923  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem21  33430  poimirlem27  33436  islln2a  34803  islpln2a  34834  islvol2aN  34878  dalem1  34945  trlnidatb  35464  lswn0  41380  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  dignn0flhalflem1  42409