Theorem necon2ad 2941

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

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

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 207  df-ne 2927

This theorem is referenced by:  necon2d  2949  prneimg  4821  tz7.2  5624  nordeq  6354  xpord3inddlem  8136  omxpenlem  9047  pr2neOLD  9965  cflim2  10223  cfslb2n  10228  ltne  11278  sqrt2irr  16224  rpexp  16699  pcgcd1  16855  plttr  18308  odhash3  19513  nzrunit  20440  lbspss  20996  en2top  22879  fbfinnfr  23735  ufileu  23813  alexsubALTlem4  23944  lebnumlem1  24867  lebnumlem2  24868  lebnumlem3  24869  ivthlem2  25360  ivthlem3  25361  dvne0  25923  deg1nn0clb  26002  lgsmod  27241  nodenselem4  27606  nodenselem5  27607  nodenselem7  27609  noinfbnd2lem1  27649  sltne  27689  slerec  27738  cuteq1  27753  addsval  27876  axlowdimlem16  28891  upgrewlkle2  29541  wlkon2n0  29601  pthdivtx  29664  normgt0  31063  pmtrcnel  33053  lindsadd  37614  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem21  37642  poimirlem27  37648  islln2a  39518  islpln2a  39549  islvol2aN  39593  dalem1  39660  trlnidatb  40178  ensucne0OLD  43526  lswn0  47449  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  dignn0flhalflem1  48608