Theorem necon2ad 2944

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  necon2d  2952  prneimg  4805  tz7.2  5602  nordeq  6330  xpord3inddlem  8090  omxpenlem  8998  cflim2  10161  cfslb2n  10166  ltne  11217  sqrt2irr  16160  rpexp  16635  pcgcd1  16791  plttr  18248  odhash3  19490  nzrunit  20441  lbspss  21018  en2top  22901  fbfinnfr  23757  ufileu  23835  alexsubALTlem4  23966  lebnumlem1  24888  lebnumlem2  24889  lebnumlem3  24890  ivthlem2  25381  ivthlem3  25382  dvne0  25944  deg1nn0clb  26023  lgsmod  27262  nodenselem4  27627  nodenselem5  27628  nodenselem7  27630  noinfbnd2lem1  27670  sltne  27710  slerec  27761  cuteq1  27779  addsval  27906  axlowdimlem16  28937  upgrewlkle2  29587  wlkon2n0  29645  pthdivtx  29707  normgt0  31109  pmtrcnel  33065  lindsadd  37673  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem21  37701  poimirlem27  37707  islln2a  39636  islpln2a  39667  islvol2aN  39711  dalem1  39778  trlnidatb  40296  ensucne0OLD  43647  lswn0  47568  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  dignn0flhalflem1  48740