Theorem necon2ad 2976

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 143	. 2 ⊢ (𝜓 → ¬ ¬ 𝜓)
2		necon2ad.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
3	2	necon3bd 2975	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 ≠ 𝐵))
4	1, 3	syl5 35	1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2962

This theorem is used by:  necon2d  2984  prneimg  4824  tz7.2  5649  nordeq  6386  xpord3inddlem  8159  omxpenlem  9076  cflim2  10265  cfslb2n  10270  ltne  11325  sqrt2irr  16330  rpexp  16806  pcgcd1  16962  plttr  18421  odhash3  19677  nzrunit  20659  lbspss  21240  en2top  23179  fbfinnfr  24035  ufileu  24113  alexsubALTlem4  24244  lebnumlem1  25157  lebnumlem2  25158  lebnumlem3  25159  ivthlem2  25648  ivthlem3  25649  dvne0  26207  deg1nn0clb  26284  lgsmod  27524  nodenselem4  27888  nodenselem5  27889  nodenselem7  27891  noinfbnd2lem1  27931  ltsne  27975  lesrec  28029  cuteq1  28047  addsval  28192  axlowdimlem16  29344  upgrewlkle2  29993  wlkon2n0  30051  pthdivtx  30113  normgt0  31516  pmtrcnel  33440  lindsadd  38305  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem21  38333  poimirlem27  38339  islln2a  40332  islpln2a  40363  islvol2aN  40407  dalem1  40474  trlnidatb  40992  ensucne0OLD  44297  lswn0  48234  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  dignn0flhalflem1  49436