Theorem necon2ad 2945

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

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

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 2931

This theorem is referenced by:  necon2d  2953  prneimg  4807  tz7.2  5604  nordeq  6333  xpord3inddlem  8093  omxpenlem  9001  cflim2  10164  cfslb2n  10169  ltne  11220  sqrt2irr  16168  rpexp  16643  pcgcd1  16799  plttr  18256  odhash3  19498  nzrunit  20449  lbspss  21026  en2top  22910  fbfinnfr  23766  ufileu  23844  alexsubALTlem4  23975  lebnumlem1  24897  lebnumlem2  24898  lebnumlem3  24899  ivthlem2  25390  ivthlem3  25391  dvne0  25953  deg1nn0clb  26032  lgsmod  27271  nodenselem4  27636  nodenselem5  27637  nodenselem7  27639  noinfbnd2lem1  27679  sltne  27719  slerec  27770  cuteq1  27788  addsval  27915  axlowdimlem16  28946  upgrewlkle2  29596  wlkon2n0  29654  pthdivtx  29716  normgt0  31118  pmtrcnel  33069  lindsadd  37663  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem21  37691  poimirlem27  37697  islln2a  39626  islpln2a  39657  islvol2aN  39701  dalem1  39768  trlnidatb  40286  ensucne0OLD  43637  lswn0  47558  nnsum4primeseven  47914  nnsum4primesevenALTV  47915  dignn0flhalflem1  48730