Theorem necon2ad 2945

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2930

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 2931

This theorem is referenced by:  necon2d  2953  prneimg  4853  tz7.2  5656  nordeq  6384  xpord3inddlem  8157  omxpenlem  9100  pr2neOLD  10038  cflim2  10294  cfslb2n  10299  ltne  11349  sqrt2irr  16243  rpexp  16716  pcgcd1  16871  plttr  18359  odhash3  19567  nzrunit  20499  lbspss  21053  en2top  22973  fbfinnfr  23830  ufileu  23908  alexsubALTlem4  24039  lebnumlem1  24972  lebnumlem2  24973  lebnumlem3  24974  ivthlem2  25466  ivthlem3  25467  dvne0  26029  deg1nn0clb  26111  lgsmod  27346  nodenselem4  27711  nodenselem5  27712  nodenselem7  27714  noinfbnd2lem1  27754  sltne  27794  slerec  27843  cuteq1  27857  addsval  27970  axlowdimlem16  28885  upgrewlkle2  29537  wlkon2n0  29597  pthdivtx  29660  normgt0  31054  pmtrcnel  32968  lindsadd  37324  poimirlem16  37347  poimirlem17  37348  poimirlem19  37350  poimirlem21  37352  poimirlem27  37358  islln2a  39226  islpln2a  39257  islvol2aN  39301  dalem1  39368  trlnidatb  39886  ensucne0OLD  43231  lswn0  47049  nnsum4primeseven  47405  nnsum4primesevenALTV  47406  dignn0flhalflem1  48036