MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon2ad Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 notnot 134 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon2ad.1 . . 3 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
32necon3bd 2795 . 2 (𝜑 → (¬ ¬ 𝜓𝐴𝐵))
41, 3syl5 33 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator