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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543   ≠ 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 210  df-ne 2933

This theorem is referenced by:  necon2d  2955  prneimg  4751  tz7.2  5520  nordeq  6210  omxpenlem  8724  pr2ne  9584  cflim2  9842  cfslb2n  9847  ltne  10894  sqrt2irr  15773  rpexp  16242  pcgcd1  16393  plttr  17802  odhash3  18919  lbspss  20073  nzrunit  20259  en2top  21836  fbfinnfr  22692  ufileu  22770  alexsubALTlem4  22901  lebnumlem1  23812  lebnumlem2  23813  lebnumlem3  23814  ivthlem2  24303  ivthlem3  24304  dvne0  24862  deg1nn0clb  24942  lgsmod  26158  axlowdimlem16  27002  upgrewlkle2  27648  wlkon2n0  27708  pthdivtx  27770  normgt0  29162  pmtrcnel  31031  nodenselem4  33576  nodenselem5  33577  nodenselem7  33579  noinfbnd2lem1  33619  slerec  33699  addsval  33812  lindsadd  35456  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem21  35484  poimirlem27  35490  islln2a  37217  islpln2a  37248  islvol2aN  37292  dalem1  37359  trlnidatb  37877  ensucne0OLD  40763  lswn0  44512  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  dignn0flhalflem1  45577