Theorem necon2ad 2972

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2958

This theorem is used by:  necon2d  2980  prneimg  4817  tz7.2  5642  nordeq  6380  xpord3inddlem  8156  omxpenlem  9080  cflim2  10269  cfslb2n  10274  ltne  11335  sqrt2irr  16343  rpexp  16819  pcgcd1  16975  plttr  18434  odhash3  19709  nzrunit  20691  lbspss  21272  en2top  23216  fbfinnfr  24073  ufileu  24151  alexsubALTlem4  24282  lebnumlem1  25195  lebnumlem2  25196  lebnumlem3  25197  ivthlem2  25686  ivthlem3  25687  dvne0  26245  deg1nn0clb  26322  lgsmod  27567  nodenselem4  27931  nodenselem5  27932  nodenselem7  27934  noinfbnd2lem1  27974  ltsne  28018  lesrec  28072  cuteq1  28090  addsval  28235  axlowdimlem16  29422  upgrewlkle2  30074  wlkon2n0  30132  pthdivtx  30199  normgt0  31616  pmtrcnel  33537  lindsadd  38375  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem21  38398  poimirlem27  38404  islln2a  40398  islpln2a  40429  islvol2aN  40473  dalem1  40540  trlnidatb  41058  ensucne0OLD  44378  lswn0  48352  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  dignn0flhalflem1  49553