Theorem necon2ad 2971

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necon2d  2979  prneimg  4814  tz7.2  5634  nordeq  6381  xpord3inddlem  8171  omxpenlem  9097  cflim2  10341  cfslb2n  10346  ltne  11407  sqrt2irr  16417  rpexp  16898  pcgcd1  17055  plttr  18514  odhash3  19790  nzrunit  20775  lbspss  21357  en2top  23303  fbfinnfr  24160  ufileu  24238  alexsubALTlem4  24369  lebnumlem1  25282  lebnumlem2  25283  lebnumlem3  25284  ivthlem2  25773  ivthlem3  25774  dvne0  26331  deg1nn0clb  26408  lgsmod  27650  nodenselem4  28044  nodenselem5  28045  nodenselem7  28047  noinfbnd2lem1  28087  ltsne  28131  lesrec  28185  cuteq1  28203  addsval  28348  axlowdimlem16  29535  upgrewlkle2  30187  wlkon2n0  30245  pthdivtx  30312  normgt0  31729  pmtrcnel  33650  lindsadd  38536  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem21  38559  poimirlem27  38565  islln2a  40574  islpln2a  40605  islvol2aN  40649  dalem1  40716  trlnidatb  41234  ensucne0OLD  44530  lswn0  48525  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  dignn0flhalflem1  49726