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

Theorem necon1ad 2634
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 2569 . 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 2567
This theorem is referenced by:  prnebg  3939  fr0  4521  onmindif2  4751  sofld  5277  suppss  5822  suppss2  6259  uniinqs  6943  dfac5lem4  7963  fin1a2lem10  8245  uzwo  10495  seqf1olem1  11317  seqf1olem2  11318  hashnncl  11600  pceq0  13199  vdwmc2  13302  odcau  15193  islss  15966  fidomndrnglem  16321  mvrf1  16444  obs2ss  16911  obslbs  16912  regr1lem2  17725  iccpnfhmeo  18923  itg10a  19555  dvlip  19830  mpfrcl  19892  deg1ge  19974  elply2  20068  coeeulem  20096  dgrle  20115  coemullem  20121  basellem2  20817  perfectlem2  20967  lgsabs1  21071  lnon0  22252  atsseq  23803  disjif2  23976  suppss2f  24002  cvmseu  24916  itg2addnclem  26155  dsmmacl  27075  lsatcmp  29486  lsatcmp2  29487  ltrnnid  30618  trlatn0  30654  cdlemh  31299  dochlkr  31868
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 2569
  Copyright terms: Public domain W3C validator