Theorem necon2ad 2957

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  necon2d  2965  prneimg  4782  tz7.2  5564  nordeq  6270  omxpenlem  8813  pr2ne  9692  cflim2  9950  cfslb2n  9955  ltne  11002  sqrt2irr  15886  rpexp  16355  pcgcd1  16506  plttr  17975  odhash3  19096  lbspss  20259  nzrunit  20451  en2top  22043  fbfinnfr  22900  ufileu  22978  alexsubALTlem4  23109  lebnumlem1  24030  lebnumlem2  24031  lebnumlem3  24032  ivthlem2  24521  ivthlem3  24522  dvne0  25080  deg1nn0clb  25160  lgsmod  26376  axlowdimlem16  27228  upgrewlkle2  27876  wlkon2n0  27936  pthdivtx  27998  normgt0  29390  pmtrcnel  31260  nodenselem4  33817  nodenselem5  33818  nodenselem7  33820  noinfbnd2lem1  33860  slerec  33940  addsval  34053  lindsadd  35697  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem21  35725  poimirlem27  35731  islln2a  37458  islpln2a  37489  islvol2aN  37533  dalem1  37600  trlnidatb  38118  ensucne0OLD  41035  lswn0  44784  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  dignn0flhalflem1  45849