Theorem necon2ad 2975

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  necon2d  2983  prneimg  4815  tz7.2  5635  nordeq  6369  xpord3inddlem  8138  omxpenlem  9054  cflim2  10235  cfslb2n  10240  ltne  11295  sqrt2irr  16295  rpexp  16771  pcgcd1  16927  plttr  18386  odhash3  19637  nzrunit  20599  lbspss  21172  en2top  23103  fbfinnfr  23959  ufileu  24037  alexsubALTlem4  24168  lebnumlem1  25081  lebnumlem2  25082  lebnumlem3  25083  ivthlem2  25572  ivthlem3  25573  dvne0  26131  deg1nn0clb  26208  lgsmod  27445  nodenselem4  27809  nodenselem5  27810  nodenselem7  27812  noinfbnd2lem1  27852  ltsne  27896  lesrec  27950  cuteq1  27968  addsval  28113  axlowdimlem16  29216  upgrewlkle2  29865  wlkon2n0  29923  pthdivtx  29985  normgt0  31388  pmtrcnel  33322  lindsadd  38124  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem21  38152  poimirlem27  38158  islln2a  40153  islpln2a  40184  islvol2aN  40228  dalem1  40295  trlnidatb  40813  ensucne0OLD  44118  lswn0  48048  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  dignn0flhalflem1  49246