Theorem necon2ad 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 206  df-ne 2944

This theorem is referenced by:  necon2d  2966  prneimg  4785  tz7.2  5573  nordeq  6285  omxpenlem  8860  pr2ne  9761  cflim2  10019  cfslb2n  10024  ltne  11072  sqrt2irr  15958  rpexp  16427  pcgcd1  16578  plttr  18060  odhash3  19181  lbspss  20344  nzrunit  20538  en2top  22135  fbfinnfr  22992  ufileu  23070  alexsubALTlem4  23201  lebnumlem1  24124  lebnumlem2  24125  lebnumlem3  24126  ivthlem2  24616  ivthlem3  24617  dvne0  25175  deg1nn0clb  25255  lgsmod  26471  axlowdimlem16  27325  upgrewlkle2  27973  wlkon2n0  28034  pthdivtx  28097  normgt0  29489  pmtrcnel  31358  nodenselem4  33890  nodenselem5  33891  nodenselem7  33893  noinfbnd2lem1  33933  slerec  34013  addsval  34126  lindsadd  35770  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem21  35798  poimirlem27  35804  islln2a  37531  islpln2a  37562  islvol2aN  37606  dalem1  37673  trlnidatb  38191  ensucne0OLD  41137  lswn0  44896  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  dignn0flhalflem1  45961