Theorem necon2ad 2950

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon2d  2958  prneimg  4792  tz7.2  5608  nordeq  6336  xpord3inddlem  8101  omxpenlem  9013  cflim2  10183  cfslb2n  10188  ltne  11241  sqrt2irr  16214  rpexp  16690  pcgcd1  16846  plttr  18304  odhash3  19549  nzrunit  20503  lbspss  21079  en2top  22975  fbfinnfr  23831  ufileu  23909  alexsubALTlem4  24040  lebnumlem1  24953  lebnumlem2  24954  lebnumlem3  24955  ivthlem2  25444  ivthlem3  25445  dvne0  26003  deg1nn0clb  26080  lgsmod  27311  nodenselem4  27676  nodenselem5  27677  nodenselem7  27679  noinfbnd2lem1  27719  ltsne  27763  lesrec  27816  cuteq1  27834  addsval  27979  axlowdimlem16  29051  upgrewlkle2  29700  wlkon2n0  29758  pthdivtx  29820  normgt0  31223  pmtrcnel  33177  lindsadd  37987  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem21  38015  poimirlem27  38021  islln2a  40016  islpln2a  40047  islvol2aN  40091  dalem1  40158  trlnidatb  40676  ensucne0OLD  43981  lswn0  47926  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  dignn0flhalflem1  49113