Theorem necon2ad 2954

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

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

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 206  df-ne 2940

This theorem is referenced by:  necon2d  2962  prneimg  4855  tz7.2  5660  nordeq  6383  xpord3inddlem  8144  omxpenlem  9077  pr2neOLD  10004  cflim2  10262  cfslb2n  10267  ltne  11316  sqrt2irr  16197  rpexp  16664  pcgcd1  16815  plttr  18300  odhash3  19486  nzrunit  20414  lbspss  20838  en2top  22709  fbfinnfr  23566  ufileu  23644  alexsubALTlem4  23775  lebnumlem1  24708  lebnumlem2  24709  lebnumlem3  24710  ivthlem2  25202  ivthlem3  25203  dvne0  25764  deg1nn0clb  25844  lgsmod  27063  nodenselem4  27427  nodenselem5  27428  nodenselem7  27430  noinfbnd2lem1  27470  sltne  27510  slerec  27558  cuteq1  27572  addsval  27685  axlowdimlem16  28483  upgrewlkle2  29131  wlkon2n0  29191  pthdivtx  29254  normgt0  30648  pmtrcnel  32521  lindsadd  36785  poimirlem16  36808  poimirlem17  36809  poimirlem19  36811  poimirlem21  36813  poimirlem27  36819  islln2a  38692  islpln2a  38723  islvol2aN  38767  dalem1  38834  trlnidatb  39352  ensucne0OLD  42584  lswn0  46411  nnsum4primeseven  46767  nnsum4primesevenALTV  46768  dignn0flhalflem1  47389