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

Theorem necon1ad 2665
Description: Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.)
Hypothesis
Ref Expression
necon1ad.1  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
Assertion
Ref Expression
necon1ad  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )

Proof of Theorem necon1ad
StepHypRef Expression
1 df-ne 2600 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon1ad.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
32con1d 118 . 2  |-  ( ph  ->  ( -.  A  =  B  ->  ps )
)
41, 3syl5bi 209 1  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  prnebg  3971  fr0  4553  onmindif2  4784  sofld  5310  suppss  5855  suppss2  6292  uniinqs  6976  dfac5lem4  7999  fin1a2lem10  8281  uzwo  10531  seqf1olem1  11354  seqf1olem2  11355  hashnncl  11637  pceq0  13236  vdwmc2  13339  odcau  15230  islss  16003  fidomndrnglem  16358  mvrf1  16481  obs2ss  16948  obslbs  16949  regr1lem2  17764  iccpnfhmeo  18962  itg10a  19594  dvlip  19869  mpfrcl  19931  deg1ge  20013  elply2  20107  coeeulem  20135  dgrle  20154  coemullem  20160  basellem2  20856  perfectlem2  21006  lgsabs1  21110  lnon0  22291  atsseq  23842  disjif2  24015  suppss2f  24041  cvmseu  24955  itg2addnclem  26246  dsmmacl  27175  lsatcmp  29738  lsatcmp2  29739  ltrnnid  30870  trlatn0  30906  cdlemh  31551  dochlkr  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2600
  Copyright terms: Public domain W3C validator