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

Theorem necon1ad 2951
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 2947 . 2 (𝜑 → (𝐴𝐵 → ¬ ¬ 𝜓))
3 notnotr 132 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2934
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 210  df-ne 2935
This theorem is referenced by:  prnebg  4741  fr0  5504  sofld  6019  onmindif2  7546  suppss  7889  suppssOLD  7890  suppss2  7895  uniinqs  8408  dfac5lem4  9626  uzwo  12393  seqf1olem1  13501  seqf1olem2  13502  hashnncl  13819  pceq0  16307  vdwmc2  16415  odcau  18847  islss  19825  fidomndrnglem  20198  obs2ss  20545  obslbs  20546  dsmmacl  20557  mvrf1  20804  mpfrcl  20899  mhpvarcl  20942  regr1lem2  22491  iccpnfhmeo  23697  itg10a  24463  dvlip  24745  deg1ge  24851  elply2  24945  coeeulem  24973  dgrle  24992  coemullem  24999  basellem2  25819  perfectlem2  25966  lgsabs1  26072  lnon0  28733  atsseq  30282  disjif2  30494  prmidl0  31198  cvmseu  32809  nosepon  33509  noextenddif  33512  matunitlindf  35398  poimirlem2  35402  poimirlem18  35418  poimirlem21  35421  itg2addnclem  35451  lsatcmp  36640  lsatcmp2  36641  ltrnnid  37773  trlatn0  37809  cdlemh  38454  dochlkr  39022  perfectALTVlem2  44708
  Copyright terms: Public domain W3C validator