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

Theorem necon1ad 2526
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 2461 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon1ad.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  A  =  B ) )
32con1d 116 . 2  |-  ( ph  ->  ( -.  A  =  B  ->  ps )
)
41, 3syl5bi 208 1  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  fr0  4388  onmindif2  4619  sofld  5137  suppss  5674  suppss2  6089  dfac5lem4  7769  fin1a2lem10  8051  uzwo  10297  seqf1olem1  11101  seqf1olem2  11102  hashnncl  11370  pceq0  12939  vdwmc2  13042  odcau  14931  dprdsn  15287  islss  15708  fidomndrnglem  16063  mvrf1  16186  obs2ss  16645  obslbs  16646  regr1lem2  17447  iccpnfhmeo  18459  itg10a  19081  dvlip  19356  mpfrcl  19418  deg1ge  19500  elply2  19594  coeeulem  19622  dgrle  19641  coemullem  19647  basellem2  20335  perfectlem2  20485  lgsabs1  20589  lnon0  21392  atsseq  22943  suppss2f  23216  cvmseu  23822  itg2addnclem  25003  uninqs  25142  cbcpcp  25265  dsmmacl  27310  lsatcmp  29815  lsatcmp2  29816  ltrnnid  30947  trlatn0  30983  cdlemh  31628  dochlkr  32197
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 177  df-ne 2461
  Copyright terms: Public domain W3C validator