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

Theorem necon1ad 2636
Description: Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon1ad.1  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
Assertion
Ref Expression
necon1ad  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )

Proof of Theorem necon1ad
StepHypRef Expression
1 necon1ad.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
21necon3ad 2630 . 2  |-  ( ph  ->  ( A  =/=  B  ->  -.  -.  ps )
)
3 notnot2 115 . 2  |-  ( -. 
-.  ps  ->  ps )
42, 3syl6 34 1  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437    =/= wne 2614
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 188  df-ne 2616
This theorem is referenced by:  prnebg  4182  fr0  4832  sofld  5303  onmindif2  6654  suppss  6957  suppss2  6961  uniinqs  7455  dfac5lem4  8565  uzwo  11230  seqf1olem1  12259  seqf1olem2  12260  hashnncl  12554  pceq0  14820  vdwmc2  14929  odcau  17256  islss  18158  fidomndrnglem  18530  mvrf1  18649  mpfrcl  18741  obs2ss  19291  obslbs  19292  dsmmacl  19303  regr1lem2  20754  iccpnfhmeo  21972  itg10a  22667  dvlip  22944  deg1ge  23046  elply2  23149  coeeulem  23177  dgrle  23196  coemullem  23203  basellem2  24007  perfectlem2  24157  lgsabs1  24261  lnon0  26438  atsseq  27999  disjif2  28194  suppss2fOLD  28240  cvmseu  30008  poimirlem2  31907  poimirlem18  31923  poimirlem21  31926  itg2addnclem  31958  lsatcmp  32539  lsatcmp2  32540  ltrnnid  33671  trlatn0  33708  cdlemh  34354  dochlkr  34923  perfectALTVlem2  38715
  Copyright terms: Public domain W3C validator