Theorem necon2ad 2971

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon2d  2979  prneimg  4811  tz7.2  5628  nordeq  6361  xpord3inddlem  8129  omxpenlem  9046  cflim2  10217  cfslb2n  10222  ltne  11277  sqrt2irr  16264  rpexp  16740  pcgcd1  16896  plttr  18355  odhash3  19599  nzrunit  20553  lbspss  21129  en2top  23025  fbfinnfr  23881  ufileu  23959  alexsubALTlem4  24090  lebnumlem1  25003  lebnumlem2  25004  lebnumlem3  25005  ivthlem2  25494  ivthlem3  25495  dvne0  26053  deg1nn0clb  26130  lgsmod  27364  nodenselem4  27728  nodenselem5  27729  nodenselem7  27731  noinfbnd2lem1  27771  ltsne  27815  lesrec  27869  cuteq1  27887  addsval  28032  axlowdimlem16  29104  upgrewlkle2  29753  wlkon2n0  29811  pthdivtx  29873  normgt0  31276  pmtrcnel  33230  lindsadd  38076  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem21  38104  poimirlem27  38110  islln2a  40105  islpln2a  40136  islvol2aN  40180  dalem1  40247  trlnidatb  40765  ensucne0OLD  44070  lswn0  48014  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  dignn0flhalflem1  49201