Theorem necon2ad 2961

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon2d  2969  prneimg  4879  tz7.2  5683  nordeq  6414  xpord3inddlem  8195  omxpenlem  9139  pr2neOLD  10074  cflim2  10332  cfslb2n  10337  ltne  11387  sqrt2irr  16297  rpexp  16769  pcgcd1  16924  plttr  18412  odhash3  19618  nzrunit  20550  lbspss  21104  en2top  23013  fbfinnfr  23870  ufileu  23948  alexsubALTlem4  24079  lebnumlem1  25012  lebnumlem2  25013  lebnumlem3  25014  ivthlem2  25506  ivthlem3  25507  dvne0  26070  deg1nn0clb  26149  lgsmod  27385  nodenselem4  27750  nodenselem5  27751  nodenselem7  27753  noinfbnd2lem1  27793  sltne  27833  slerec  27882  cuteq1  27896  addsval  28013  axlowdimlem16  28990  upgrewlkle2  29642  wlkon2n0  29702  pthdivtx  29765  normgt0  31159  pmtrcnel  33082  lindsadd  37573  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem21  37601  poimirlem27  37607  islln2a  39474  islpln2a  39505  islvol2aN  39549  dalem1  39616  trlnidatb  40134  ensucne0OLD  43492  lswn0  47318  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  dignn0flhalflem1  48349