Theorem necon2ad 2976

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1507   ≠ wne 2961

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 199  df-ne 2962

This theorem is referenced by:  necon2d  2984  prneimg  4653  tz7.2  5385  nordeq  6042  omxpenlem  8408  pr2ne  9219  cflim2  9477  cfslb2n  9482  ltne  10531  sqrt2irr  15456  rpexp  15914  pcgcd1  16063  plttr  17432  odhash3  18456  lbspss  19570  nzrunit  19755  en2top  21291  fbfinnfr  22147  ufileu  22225  alexsubALTlem4  22356  lebnumlem1  23262  lebnumlem2  23263  lebnumlem3  23264  ivthlem2  23750  ivthlem3  23751  dvne0  24305  deg1nn0clb  24381  lgsmod  25595  axlowdimlem16  26440  upgrewlkle2  27085  wlkon2n0  27144  pthdivtx  27212  normgt0  28677  nodenselem4  32712  nodenselem5  32713  nodenselem7  32715  slerec  32798  lindsadd  34326  poimirlem16  34349  poimirlem17  34350  poimirlem19  34352  poimirlem21  34354  poimirlem27  34360  islln2a  36098  islpln2a  36129  islvol2aN  36173  dalem1  36240  trlnidatb  36758  lswn0  42976  nnsum4primeseven  43333  nnsum4primesevenALTV  43334  dignn0flhalflem1  44043