Theorem necon2ad 2940

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon2d  2948  prneimg  4818  tz7.2  5621  nordeq  6351  xpord3inddlem  8133  omxpenlem  9042  pr2neOLD  9958  cflim2  10216  cfslb2n  10221  ltne  11271  sqrt2irr  16217  rpexp  16692  pcgcd1  16848  plttr  18301  odhash3  19506  nzrunit  20433  lbspss  20989  en2top  22872  fbfinnfr  23728  ufileu  23806  alexsubALTlem4  23937  lebnumlem1  24860  lebnumlem2  24861  lebnumlem3  24862  ivthlem2  25353  ivthlem3  25354  dvne0  25916  deg1nn0clb  25995  lgsmod  27234  nodenselem4  27599  nodenselem5  27600  nodenselem7  27602  noinfbnd2lem1  27642  sltne  27682  slerec  27731  cuteq1  27746  addsval  27869  axlowdimlem16  28884  upgrewlkle2  29534  wlkon2n0  29594  pthdivtx  29657  normgt0  31056  pmtrcnel  33046  lindsadd  37607  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem21  37635  poimirlem27  37641  islln2a  39511  islpln2a  39542  islvol2aN  39586  dalem1  39653  trlnidatb  40171  ensucne0OLD  43519  lswn0  47445  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  dignn0flhalflem1  48604