Theorem necon2ad 2954

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

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

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 206  df-ne 2940

This theorem is referenced by:  necon2d  2962  prneimg  4817  tz7.2  5622  nordeq  6341  xpord3inddlem  8091  omxpenlem  9024  pr2neOLD  9950  cflim2  10208  cfslb2n  10213  ltne  11261  sqrt2irr  16142  rpexp  16609  pcgcd1  16760  plttr  18245  odhash3  19372  nzrunit  20211  lbspss  20600  en2top  22372  fbfinnfr  23229  ufileu  23307  alexsubALTlem4  23438  lebnumlem1  24361  lebnumlem2  24362  lebnumlem3  24363  ivthlem2  24853  ivthlem3  24854  dvne0  25412  deg1nn0clb  25492  lgsmod  26708  nodenselem4  27072  nodenselem5  27073  nodenselem7  27075  noinfbnd2lem1  27115  slerec  27201  addsval  27317  axlowdimlem16  27969  upgrewlkle2  28617  wlkon2n0  28677  pthdivtx  28740  normgt0  30132  pmtrcnel  32010  lindsadd  36144  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem21  36172  poimirlem27  36178  islln2a  38053  islpln2a  38084  islvol2aN  38128  dalem1  38195  trlnidatb  38713  ensucne0OLD  41924  lswn0  45756  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  dignn0flhalflem1  46821