Theorem necon2ad 2956

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2941

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 2942

This theorem is referenced by:  necon2d  2964  prneimg  4797  tz7.2  5592  nordeq  6308  omxpenlem  8917  pr2neOLD  9841  cflim2  10099  cfslb2n  10104  ltne  11152  sqrt2irr  16037  rpexp  16504  pcgcd1  16655  plttr  18137  odhash3  19257  lbspss  20427  nzrunit  20621  en2top  22218  fbfinnfr  23075  ufileu  23153  alexsubALTlem4  23284  lebnumlem1  24207  lebnumlem2  24208  lebnumlem3  24209  ivthlem2  24699  ivthlem3  24700  dvne0  25258  deg1nn0clb  25338  lgsmod  26554  nodenselem4  26918  nodenselem5  26919  nodenselem7  26921  axlowdimlem16  27461  upgrewlkle2  28109  wlkon2n0  28170  pthdivtx  28233  normgt0  29625  pmtrcnel  31493  noinfbnd2lem1  34007  slerec  34087  addsval  34200  lindsadd  35842  poimirlem16  35865  poimirlem17  35866  poimirlem19  35868  poimirlem21  35870  poimirlem27  35876  islln2a  37752  islpln2a  37783  islvol2aN  37827  dalem1  37894  trlnidatb  38412  ensucne0OLD  41371  lswn0  45161  nnsum4primeseven  45517  nnsum4primesevenALTV  45518  dignn0flhalflem1  46226