Theorem necon2ad 2970

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

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

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 2956

This theorem is used by:  necon2d  2978  prneimg  4808  tz7.2  5633  nordeq  6381  xpord3inddlem  8173  omxpenlem  9100  cflim2  10344  cfslb2n  10349  ltne  11410  sqrt2irr  16422  rpexp  16903  pcgcd1  17060  plttr  18519  odhash3  19795  nzrunit  20780  lbspss  21362  en2top  23308  fbfinnfr  24165  ufileu  24243  alexsubALTlem4  24374  lebnumlem1  25287  lebnumlem2  25288  lebnumlem3  25289  ivthlem2  25778  ivthlem3  25779  dvne0  26336  deg1nn0clb  26413  lgsmod  27655  nodenselem4  28049  nodenselem5  28050  nodenselem7  28052  noinfbnd2lem1  28092  ltsne  28136  lesrec  28190  cuteq1  28208  addsval  28353  axlowdimlem16  29540  upgrewlkle2  30192  wlkon2n0  30250  pthdivtx  30317  normgt0  31734  pmtrcnel  33696  lindsadd  38629  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem21  38652  poimirlem27  38658  islln2a  40667  islpln2a  40698  islvol2aN  40742  dalem1  40809  trlnidatb  41327  ensucne0OLD  44624  lswn0  48619  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  dignn0flhalflem1  49820