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

Theorem necon1ad 2793
Description: Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon1ad.1 (𝜑 → (¬ 𝜓𝐴 = 𝐵))
Assertion
Ref Expression
necon1ad (𝜑 → (𝐴𝐵𝜓))

Proof of Theorem necon1ad
StepHypRef Expression
1 necon1ad.1 . . 3 (𝜑 → (¬ 𝜓𝐴 = 𝐵))
21necon3ad 2789 . 2 (𝜑 → (𝐴𝐵 → ¬ ¬ 𝜓))
3 notnotr 123 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 34 1 (𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2774
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 2776
This theorem is referenced by:  prnebg  4319  fr0  5002  sofld  5481  onmindif2  6876  suppss  7184  suppss2  7188  uniinqs  7686  dfac5lem4  8804  uzwo  11578  seqf1olem1  12652  seqf1olem2  12653  hashnncl  12965  pceq0  15354  vdwmc2  15462  odcau  17783  islss  18697  fidomndrnglem  19068  mvrf1  19187  mpfrcl  19280  obs2ss  19829  obslbs  19830  dsmmacl  19841  regr1lem2  21290  iccpnfhmeo  22478  itg10a  23195  dvlip  23472  deg1ge  23574  elply2  23668  coeeulem  23696  dgrle  23715  coemullem  23722  basellem2  24520  perfectlem2  24667  lgsabs1  24773  lnon0  26838  atsseq  28391  disjif2  28577  cvmseu  30313  nosepon  30867  matunitlindf  32375  poimirlem2  32379  poimirlem18  32395  poimirlem21  32398  itg2addnclem  32429  lsatcmp  33106  lsatcmp2  33107  ltrnnid  34238  trlatn0  34275  cdlemh  34921  dochlkr  35490  perfectALTVlem2  39965
  Copyright terms: Public domain W3C validator