Theorem necon2ad 2974

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

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

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 2960

This theorem is used by:  necon2d  2982  prneimg  4812  tz7.2  5638  nordeq  6399  xpord3inddlem  8198  omxpenlem  9125  cflim2  10368  cfslb2n  10373  ltne  11434  sqrt2irr  16446  rpexp  16927  pcgcd1  17084  plttr  18543  odhash3  19820  nzrunit  20805  lbspss  21387  en2top  23333  fbfinnfr  24190  ufileu  24268  alexsubALTlem4  24399  lebnumlem1  25312  lebnumlem2  25313  lebnumlem3  25314  ivthlem2  25803  ivthlem3  25804  dvne0  26361  deg1nn0clb  26438  lgsmod  27680  nodenselem4  28074  nodenselem5  28075  nodenselem7  28077  noinfbnd2lem1  28117  ltsne  28161  lesrec  28215  cuteq1  28233  addsval  28378  axlowdimlem16  29565  upgrewlkle2  30217  wlkon2n0  30275  pthdivtx  30342  normgt0  31759  pmtrcnel  33720  lindsadd  38728  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem21  38751  poimirlem27  38757  islln2a  40766  islpln2a  40797  islvol2aN  40841  dalem1  40908  trlnidatb  41426  ensucne0OLD  44723  lswn0  48731  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  dignn0flhalflem1  49932