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  4812  tz7.2  5615  nordeq  6344  xpord3inddlem  8106  omxpenlem  9018  cflim2  10185  cfslb2n  10190  ltne  11242  sqrt2irr  16186  rpexp  16661  pcgcd1  16817  plttr  18275  odhash3  19517  nzrunit  20469  lbspss  21046  en2top  22941  fbfinnfr  23797  ufileu  23875  alexsubALTlem4  24006  lebnumlem1  24928  lebnumlem2  24929  lebnumlem3  24930  ivthlem2  25421  ivthlem3  25422  dvne0  25984  deg1nn0clb  26063  lgsmod  27302  nodenselem4  27667  nodenselem5  27668  nodenselem7  27670  noinfbnd2lem1  27710  ltsne  27754  lesrec  27807  cuteq1  27825  addsval  27970  axlowdimlem16  29042  upgrewlkle2  29692  wlkon2n0  29750  pthdivtx  29812  normgt0  31214  pmtrcnel  33182  lindsadd  37858  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem21  37886  poimirlem27  37892  islln2a  39887  islpln2a  39918  islvol2aN  39962  dalem1  40029  trlnidatb  40547  ensucne0OLD  43880  lswn0  47798  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  dignn0flhalflem1  48969