Theorem necon2ad 2947

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  necon2d  2955  prneimg  4797  tz7.2  5614  nordeq  6342  xpord3inddlem  8104  omxpenlem  9016  cflim2  10185  cfslb2n  10190  ltne  11243  sqrt2irr  16216  rpexp  16692  pcgcd1  16848  plttr  18306  odhash3  19551  nzrunit  20501  lbspss  21077  en2top  22950  fbfinnfr  23806  ufileu  23884  alexsubALTlem4  24015  lebnumlem1  24928  lebnumlem2  24929  lebnumlem3  24930  ivthlem2  25419  ivthlem3  25420  dvne0  25978  deg1nn0clb  26055  lgsmod  27286  nodenselem4  27651  nodenselem5  27652  nodenselem7  27654  noinfbnd2lem1  27694  ltsne  27738  lesrec  27791  cuteq1  27809  addsval  27954  axlowdimlem16  29026  upgrewlkle2  29675  wlkon2n0  29733  pthdivtx  29795  normgt0  31198  pmtrcnel  33150  lindsadd  37934  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem21  37962  poimirlem27  37968  islln2a  39963  islpln2a  39994  islvol2aN  40038  dalem1  40105  trlnidatb  40623  ensucne0OLD  43957  lswn0  47904  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  dignn0flhalflem1  49091