Theorem necon2ad 3031

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 3016

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 3017

This theorem is referenced by:  necon2d  3039  prneimg  4784  tz7.2  5538  nordeq  6209  omxpenlem  8617  pr2ne  9430  cflim2  9684  cfslb2n  9689  ltne  10736  sqrt2irr  15601  rpexp  16063  pcgcd1  16212  plttr  17579  odhash3  18700  lbspss  19853  nzrunit  20039  en2top  21592  fbfinnfr  22448  ufileu  22526  alexsubALTlem4  22657  lebnumlem1  23564  lebnumlem2  23565  lebnumlem3  23566  ivthlem2  24052  ivthlem3  24053  dvne0  24607  deg1nn0clb  24683  lgsmod  25898  axlowdimlem16  26742  upgrewlkle2  27387  wlkon2n0  27447  pthdivtx  27509  normgt0  28903  pmtrcnel  30733  nodenselem4  33191  nodenselem5  33192  nodenselem7  33194  slerec  33277  lindsadd  34884  poimirlem16  34907  poimirlem17  34908  poimirlem19  34910  poimirlem21  34912  poimirlem27  34918  islln2a  36652  islpln2a  36683  islvol2aN  36727  dalem1  36794  trlnidatb  37312  ensucne0OLD  39894  lswn0  43603  nnsum4primeseven  43964  nnsum4primesevenALTV  43965  dignn0flhalflem1  44674