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

Theorem necon1ad 2683
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 2677 . 2  |-  ( ph  ->  ( A  =/=  B  ->  -.  -.  ps )
)
3 notnot2 112 . 2  |-  ( -. 
-.  ps  ->  ps )
42, 3syl6 33 1  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1379    =/= wne 2662
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 185  df-ne 2664
This theorem is referenced by:  prnebg  4214  fr0  4864  sofld  5461  suppssOLD  6021  suppss2OLD  6525  onmindif2  6642  suppss  6942  suppss2  6946  uniinqs  7403  dfac5lem4  8519  uzwo  11156  seqf1olem1  12126  seqf1olem2  12127  hashnncl  12416  pceq0  14269  vdwmc2  14372  odcau  16495  islss  17450  fidomndrnglem  17823  mvrf1  17949  mpfrcl  18055  obs2ss  18627  obslbs  18628  dsmmacl  18639  regr1lem2  20107  iccpnfhmeo  21311  itg10a  21983  dvlip  22260  deg1ge  22365  elply2  22459  coeeulem  22487  dgrle  22506  coemullem  22512  basellem2  23219  perfectlem2  23369  lgsabs1  23473  lnon0  25544  atsseq  27097  disjif2  27273  suppss2f  27308  cvmseu  28553  itg2addnclem  30000  lsatcmp  34206  lsatcmp2  34207  ltrnnid  35338  trlatn0  35374  cdlemh  36019  dochlkr  36588
  Copyright terms: Public domain W3C validator