Theorem necon2ad 2838

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon2d  2846  prneimg  4419  tz7.2  5127  nordeq  5780  omxpenlem  8102  pr2ne  8866  cflim2  9123  cfslb2n  9128  ltne  10172  sqrt2irr  15023  rpexp  15479  pcgcd1  15628  plttr  17017  odhash3  18037  lbspss  19130  nzrunit  19315  en2top  20837  fbfinnfr  21692  ufileu  21770  alexsubALTlem4  21901  lebnumlem1  22807  lebnumlem2  22808  lebnumlem3  22809  ivthlem2  23267  ivthlem3  23268  dvne0  23819  deg1nn0clb  23895  lgsmod  25093  axlowdimlem16  25882  upgrewlkle2  26558  wlkon2n0  26618  pthdivtx  26681  normgt0  28112  nodenselem4  31962  nodenselem5  31963  nodenselem7  31965  slerec  32048  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem21  33560  poimirlem27  33566  islln2a  35121  islpln2a  35152  islvol2aN  35196  dalem1  35263  trlnidatb  35782  lswn0  41705  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  dignn0flhalflem1  42734