Theorem necon2ad 2796

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1474   ≠ wne 2779

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 195  df-ne 2781

This theorem is referenced by:  necon2d  2804  prneimg  4323  tz7.2  5011  nordeq  5644  omxpenlem  7923  pr2ne  8688  cflim2  8945  cfslb2n  8950  ltne  9985  sqrt2irr  14765  rpexp  15218  pcgcd1  15367  plttr  16741  odhash3  17762  lbspss  18851  nzrunit  19036  en2top  20547  fbfinnfr  21402  ufileu  21480  alexsubALTlem4  21611  lebnumlem1  22515  lebnumlem2  22516  lebnumlem3  22517  ivthlem2  22972  ivthlem3  22973  dvne0  23522  deg1nn0clb  23598  lgsmod  24792  axlowdimlem16  25582  normgt0  27161  nofulllem4  30897  poimirlem16  32378  poimirlem17  32379  poimirlem19  32381  poimirlem21  32383  poimirlem27  32389  islln2a  33604  islpln2a  33635  islvol2aN  33679  dalem1  33746  trlnidatb  34265  nnsum4primeseven  40000  nnsum4primesevenALTV  40001  lswn0  40026  upgrewlkle2  40789  wlkOn2n0  40855  pthdivtx  40916  dignn0flhalflem1  42188