Theorem necon2ad 2948

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  necon2d  2956  prneimg  4835  tz7.2  5642  nordeq  6376  xpord3inddlem  8158  omxpenlem  9092  pr2neOLD  10024  cflim2  10282  cfslb2n  10287  ltne  11337  sqrt2irr  16272  rpexp  16746  pcgcd1  16902  plttr  18357  odhash3  19562  nzrunit  20489  lbspss  21045  en2top  22928  fbfinnfr  23784  ufileu  23862  alexsubALTlem4  23993  lebnumlem1  24916  lebnumlem2  24917  lebnumlem3  24918  ivthlem2  25410  ivthlem3  25411  dvne0  25973  deg1nn0clb  26052  lgsmod  27291  nodenselem4  27656  nodenselem5  27657  nodenselem7  27659  noinfbnd2lem1  27699  sltne  27739  slerec  27788  cuteq1  27803  addsval  27926  axlowdimlem16  28941  upgrewlkle2  29591  wlkon2n0  29651  pthdivtx  29714  normgt0  31113  pmtrcnel  33105  lindsadd  37642  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem21  37670  poimirlem27  37676  islln2a  39541  islpln2a  39572  islvol2aN  39616  dalem1  39683  trlnidatb  40201  ensucne0OLD  43529  lswn0  47438  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  dignn0flhalflem1  48575