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

Theorem necon1ad 2617
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 2552 . 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 1649    =/= wne 2550
This theorem is referenced by:  prnebg  3921  fr0  4502  onmindif2  4732  sofld  5258  suppss  5802  suppss2  6239  uniinqs  6920  dfac5lem4  7940  fin1a2lem10  8222  uzwo  10471  seqf1olem1  11289  seqf1olem2  11290  hashnncl  11572  pceq0  13171  vdwmc2  13274  odcau  15165  islss  15938  fidomndrnglem  16293  mvrf1  16416  obs2ss  16879  obslbs  16880  regr1lem2  17693  iccpnfhmeo  18841  itg10a  19469  dvlip  19744  mpfrcl  19806  deg1ge  19888  elply2  19982  coeeulem  20010  dgrle  20029  coemullem  20035  basellem2  20731  perfectlem2  20881  lgsabs1  20985  lnon0  22147  atsseq  23698  disjif2  23867  suppss2f  23892  cvmseu  24742  itg2addnclem  25957  dsmmacl  26876  lsatcmp  29118  lsatcmp2  29119  ltrnnid  30250  trlatn0  30286  cdlemh  30931  dochlkr  31500
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 2552
  Copyright terms: Public domain W3C validator