Theorem necon2ad 2943

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	⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Assertion

Ref	Expression
necon2ad	⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

Proof of Theorem necon2ad

Step	Hyp	Ref	Expression
1		notnot 142	. 2 ⊢ (𝜓 → ¬ ¬ 𝜓)
2		necon2ad.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
3	2	necon3bd 2942	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 ≠ 𝐵))
4	1, 3	syl5 34	1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 207  df-ne 2929

This theorem is referenced by:  necon2d  2951  prneimg  4806  tz7.2  5599  nordeq  6325  xpord3inddlem  8084  omxpenlem  8991  cflim2  10151  cfslb2n  10156  ltne  11207  sqrt2irr  16155  rpexp  16630  pcgcd1  16786  plttr  18243  odhash3  19486  nzrunit  20437  lbspss  21014  en2top  22898  fbfinnfr  23754  ufileu  23832  alexsubALTlem4  23963  lebnumlem1  24885  lebnumlem2  24886  lebnumlem3  24887  ivthlem2  25378  ivthlem3  25379  dvne0  25941  deg1nn0clb  26020  lgsmod  27259  nodenselem4  27624  nodenselem5  27625  nodenselem7  27627  noinfbnd2lem1  27667  sltne  27707  slerec  27758  cuteq1  27776  addsval  27903  axlowdimlem16  28933  upgrewlkle2  29583  wlkon2n0  29641  pthdivtx  29703  normgt0  31102  pmtrcnel  33053  lindsadd  37652  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem21  37680  poimirlem27  37686  islln2a  39555  islpln2a  39586  islvol2aN  39630  dalem1  39697  trlnidatb  40215  ensucne0OLD  43562  lswn0  47474  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  dignn0flhalflem1  48646