Theorem necon2ad 2947

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  necon2d  2955  prneimg  4810  tz7.2  5607  nordeq  6336  xpord3inddlem  8096  omxpenlem  9006  cflim2  10173  cfslb2n  10178  ltne  11230  sqrt2irr  16174  rpexp  16649  pcgcd1  16805  plttr  18263  odhash3  19505  nzrunit  20457  lbspss  21034  en2top  22929  fbfinnfr  23785  ufileu  23863  alexsubALTlem4  23994  lebnumlem1  24916  lebnumlem2  24917  lebnumlem3  24918  ivthlem2  25409  ivthlem3  25410  dvne0  25972  deg1nn0clb  26051  lgsmod  27290  nodenselem4  27655  nodenselem5  27656  nodenselem7  27658  noinfbnd2lem1  27698  ltsne  27742  lesrec  27795  cuteq1  27813  addsval  27958  axlowdimlem16  29030  upgrewlkle2  29680  wlkon2n0  29738  pthdivtx  29800  normgt0  31202  pmtrcnel  33171  lindsadd  37810  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem21  37838  poimirlem27  37844  islln2a  39773  islpln2a  39804  islvol2aN  39848  dalem1  39915  trlnidatb  40433  ensucne0OLD  43767  lswn0  47686  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  dignn0flhalflem1  48857