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  4808  tz7.2  5606  nordeq  6330  xpord3inddlem  8094  omxpenlem  9002  cflim2  10176  cfslb2n  10181  ltne  11231  sqrt2irr  16176  rpexp  16651  pcgcd1  16807  plttr  18264  odhash3  19473  nzrunit  20427  lbspss  21004  en2top  22888  fbfinnfr  23744  ufileu  23822  alexsubALTlem4  23953  lebnumlem1  24876  lebnumlem2  24877  lebnumlem3  24878  ivthlem2  25369  ivthlem3  25370  dvne0  25932  deg1nn0clb  26011  lgsmod  27250  nodenselem4  27615  nodenselem5  27616  nodenselem7  27618  noinfbnd2lem1  27658  sltne  27698  slerec  27748  cuteq1  27766  addsval  27892  axlowdimlem16  28920  upgrewlkle2  29570  wlkon2n0  29628  pthdivtx  29690  normgt0  31089  pmtrcnel  33044  lindsadd  37592  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem21  37620  poimirlem27  37626  islln2a  39496  islpln2a  39527  islvol2aN  39571  dalem1  39638  trlnidatb  40156  ensucne0OLD  43503  lswn0  47429  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  dignn0flhalflem1  48601