Theorem necon2ad 2971

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

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

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 2957

This theorem is used by:  necon2d  2979  prneimg  4814  tz7.2  5634  nordeq  6374  xpord3inddlem  8155  omxpenlem  9081  cflim2  10322  cfslb2n  10327  ltne  11388  sqrt2irr  16397  rpexp  16878  pcgcd1  17035  plttr  18494  odhash3  19770  nzrunit  20755  lbspss  21337  en2top  23283  fbfinnfr  24140  ufileu  24218  alexsubALTlem4  24349  lebnumlem1  25262  lebnumlem2  25263  lebnumlem3  25264  ivthlem2  25753  ivthlem3  25754  dvne0  26311  deg1nn0clb  26388  lgsmod  27632  nodenselem4  28026  nodenselem5  28027  nodenselem7  28029  noinfbnd2lem1  28069  ltsne  28113  lesrec  28167  cuteq1  28185  addsval  28330  axlowdimlem16  29517  upgrewlkle2  30169  wlkon2n0  30227  pthdivtx  30294  normgt0  31711  pmtrcnel  33632  lindsadd  38504  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem21  38527  poimirlem27  38533  islln2a  40542  islpln2a  40573  islvol2aN  40617  dalem1  40684  trlnidatb  41202  ensucne0OLD  44489  lswn0  48470  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  dignn0flhalflem1  49671