Theorem necon2ad 3033

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  necon2d  3041  prneimg  4787  tz7.2  5541  nordeq  6212  omxpenlem  8620  pr2ne  9433  cflim2  9687  cfslb2n  9692  ltne  10739  sqrt2irr  15604  rpexp  16066  pcgcd1  16215  plttr  17582  odhash3  18703  lbspss  19856  nzrunit  20042  en2top  21595  fbfinnfr  22451  ufileu  22529  alexsubALTlem4  22660  lebnumlem1  23567  lebnumlem2  23568  lebnumlem3  23569  ivthlem2  24055  ivthlem3  24056  dvne0  24610  deg1nn0clb  24686  lgsmod  25901  axlowdimlem16  26745  upgrewlkle2  27390  wlkon2n0  27450  pthdivtx  27512  normgt0  28906  pmtrcnel  30735  nodenselem4  33193  nodenselem5  33194  nodenselem7  33196  slerec  33279  lindsadd  34887  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem21  34915  poimirlem27  34921  islln2a  36655  islpln2a  36686  islvol2aN  36730  dalem1  36797  trlnidatb  37315  ensucne0OLD  39903  lswn0  43611  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  dignn0flhalflem1  44682