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

Theorem necon1ad 2949
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 2945 . 2 (𝜑 → (𝐴𝐵 → ¬ ¬ 𝜓))
3 notnotr 125 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1632  wne 2932
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 197  df-ne 2933
This theorem is referenced by:  prnebg  4533  fr0  5245  sofld  5739  onmindif2  7177  suppss  7494  suppss2  7498  uniinqs  7994  dfac5lem4  9139  uzwo  11944  seqf1olem1  13034  seqf1olem2  13035  hashnncl  13349  pceq0  15777  vdwmc2  15885  odcau  18219  islss  19137  fidomndrnglem  19508  mvrf1  19627  mpfrcl  19720  obs2ss  20275  obslbs  20276  dsmmacl  20287  regr1lem2  21745  iccpnfhmeo  22945  itg10a  23676  dvlip  23955  deg1ge  24057  elply2  24151  coeeulem  24179  dgrle  24198  coemullem  24205  basellem2  25007  perfectlem2  25154  lgsabs1  25260  lnon0  27962  atsseq  29515  disjif2  29701  cvmseu  31565  nosepon  32124  noextenddif  32127  matunitlindf  33720  poimirlem2  33724  poimirlem18  33740  poimirlem21  33743  itg2addnclem  33774  lsatcmp  34793  lsatcmp2  34794  ltrnnid  35925  trlatn0  35962  cdlemh  36607  dochlkr  37176  perfectALTVlem2  42141
  Copyright terms: Public domain W3C validator