Theorem necon2ad 2797

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon2d  2805  prneimg  4328  tz7.2  5022  nordeq  5659  omxpenlem  7946  pr2ne  8711  cflim2  8968  cfslb2n  8973  ltne  10013  sqrt2irr  14817  rpexp  15270  pcgcd1  15419  plttr  16793  odhash3  17814  lbspss  18903  nzrunit  19088  en2top  20600  fbfinnfr  21455  ufileu  21533  alexsubALTlem4  21664  lebnumlem1  22568  lebnumlem2  22569  lebnumlem3  22570  ivthlem2  23028  ivthlem3  23029  dvne0  23578  deg1nn0clb  23654  lgsmod  24848  axlowdimlem16  25637  normgt0  27368  nofulllem4  31104  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem21  32600  poimirlem27  32606  islln2a  33821  islpln2a  33852  islvol2aN  33896  dalem1  33963  trlnidatb  34482  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  lswn0  40242  upgrewlkle2  40808  wlkOn2n0  40874  pthdivtx  40935  dignn0flhalflem1  42207