Theorem necon2ad 2953

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

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

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 2939

This theorem is referenced by:  necon2d  2961  prneimg  4854  tz7.2  5659  nordeq  6382  xpord3inddlem  8142  omxpenlem  9075  pr2neOLD  10002  cflim2  10260  cfslb2n  10265  ltne  11315  sqrt2irr  16196  rpexp  16663  pcgcd1  16814  plttr  18299  odhash3  19485  nzrunit  20413  lbspss  20837  en2top  22708  fbfinnfr  23565  ufileu  23643  alexsubALTlem4  23774  lebnumlem1  24707  lebnumlem2  24708  lebnumlem3  24709  ivthlem2  25201  ivthlem3  25202  dvne0  25763  deg1nn0clb  25843  lgsmod  27062  nodenselem4  27426  nodenselem5  27427  nodenselem7  27429  noinfbnd2lem1  27469  sltne  27509  slerec  27557  cuteq1  27571  addsval  27684  axlowdimlem16  28482  upgrewlkle2  29130  wlkon2n0  29190  pthdivtx  29253  normgt0  30647  pmtrcnel  32520  lindsadd  36784  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem21  36812  poimirlem27  36818  islln2a  38691  islpln2a  38722  islvol2aN  38766  dalem1  38833  trlnidatb  39351  ensucne0OLD  42583  lswn0  46410  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  dignn0flhalflem1  47388