Theorem necon2ad 2948

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 2947	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 ≠ 𝐵))
4	1, 3	syl5 34	1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon2d  2956  prneimg  4798  tz7.2  5607  nordeq  6336  xpord3inddlem  8097  omxpenlem  9009  cflim2  10176  cfslb2n  10181  ltne  11234  sqrt2irr  16207  rpexp  16683  pcgcd1  16839  plttr  18297  odhash3  19542  nzrunit  20492  lbspss  21069  en2top  22960  fbfinnfr  23816  ufileu  23894  alexsubALTlem4  24025  lebnumlem1  24938  lebnumlem2  24939  lebnumlem3  24940  ivthlem2  25429  ivthlem3  25430  dvne0  25988  deg1nn0clb  26065  lgsmod  27300  nodenselem4  27665  nodenselem5  27666  nodenselem7  27668  noinfbnd2lem1  27708  ltsne  27752  lesrec  27805  cuteq1  27823  addsval  27968  axlowdimlem16  29040  upgrewlkle2  29690  wlkon2n0  29748  pthdivtx  29810  normgt0  31213  pmtrcnel  33165  lindsadd  37948  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem21  37976  poimirlem27  37982  islln2a  39977  islpln2a  40008  islvol2aN  40052  dalem1  40119  trlnidatb  40637  ensucne0OLD  43975  lswn0  47916  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  dignn0flhalflem1  49103