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

Theorem necon1ad 3030
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 3026 . 2 (𝜑 → (𝐴𝐵 → ¬ ¬ 𝜓))
3 notnotr 132 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3013
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 208  df-ne 3014
This theorem is referenced by:  prnebg  4778  fr0  5527  sofld  6037  onmindif2  7516  suppss  7849  suppss2  7853  uniinqs  8366  dfac5lem4  9540  uzwo  12299  seqf1olem1  13397  seqf1olem2  13398  hashnncl  13715  pceq0  16195  vdwmc2  16303  odcau  18658  islss  19635  fidomndrnglem  20007  mvrf1  20133  mpfrcl  20226  obs2ss  20801  obslbs  20802  dsmmacl  20813  regr1lem2  22276  iccpnfhmeo  23476  itg10a  24238  dvlip  24517  deg1ge  24619  elply2  24713  coeeulem  24741  dgrle  24760  coemullem  24767  basellem2  25586  perfectlem2  25733  lgsabs1  25839  lnon0  28502  atsseq  30051  disjif2  30259  cvmseu  32420  nosepon  33069  noextenddif  33072  matunitlindf  34771  poimirlem2  34775  poimirlem18  34791  poimirlem21  34794  itg2addnclem  34824  lsatcmp  36019  lsatcmp2  36020  ltrnnid  37152  trlatn0  37188  cdlemh  37833  dochlkr  38401  perfectALTVlem2  43764
  Copyright terms: Public domain W3C validator