Theorem necon2ad 2953

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  necon2d  2961  prneimg  4859  tz7.2  5672  nordeq  6405  xpord3inddlem  8178  omxpenlem  9112  pr2neOLD  10043  cflim2  10301  cfslb2n  10306  ltne  11356  sqrt2irr  16282  rpexp  16756  pcgcd1  16911  plttr  18400  odhash3  19609  nzrunit  20541  lbspss  21099  en2top  23008  fbfinnfr  23865  ufileu  23943  alexsubALTlem4  24074  lebnumlem1  25007  lebnumlem2  25008  lebnumlem3  25009  ivthlem2  25501  ivthlem3  25502  dvne0  26065  deg1nn0clb  26144  lgsmod  27382  nodenselem4  27747  nodenselem5  27748  nodenselem7  27750  noinfbnd2lem1  27790  sltne  27830  slerec  27879  cuteq1  27893  addsval  28010  axlowdimlem16  28987  upgrewlkle2  29639  wlkon2n0  29699  pthdivtx  29762  normgt0  31156  pmtrcnel  33092  lindsadd  37600  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem21  37628  poimirlem27  37634  islln2a  39500  islpln2a  39531  islvol2aN  39575  dalem1  39642  trlnidatb  40160  ensucne0OLD  43520  lswn0  47369  nnsum4primeseven  47725  nnsum4primesevenALTV  47726  dignn0flhalflem1  48465