Theorem necon2ad 2973

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necon2d  2981  prneimg  4820  tz7.2  5646  nordeq  6381  xpord3inddlem  8151  omxpenlem  9067  cflim2  10248  cfslb2n  10253  ltne  11308  sqrt2irr  16306  rpexp  16782  pcgcd1  16938  plttr  18397  odhash3  19647  nzrunit  20609  lbspss  21184  en2top  23123  fbfinnfr  23979  ufileu  24057  alexsubALTlem4  24188  lebnumlem1  25101  lebnumlem2  25102  lebnumlem3  25103  ivthlem2  25592  ivthlem3  25593  dvne0  26151  deg1nn0clb  26228  lgsmod  27465  nodenselem4  27829  nodenselem5  27830  nodenselem7  27832  noinfbnd2lem1  27872  ltsne  27916  lesrec  27970  cuteq1  27988  addsval  28133  axlowdimlem16  29285  upgrewlkle2  29934  wlkon2n0  29992  pthdivtx  30054  normgt0  31457  pmtrcnel  33387  lindsadd  38242  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem21  38270  poimirlem27  38276  islln2a  40269  islpln2a  40300  islvol2aN  40344  dalem1  40411  trlnidatb  40929  ensucne0OLD  44236  lswn0  48170  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  dignn0flhalflem1  49372