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

Theorem necon1ad 2513
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 2448 . 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 1623    =/= wne 2446
This theorem is referenced by:  fr0  4372  onmindif2  4603  sofld  5121  suppss  5658  suppss2  6073  dfac5lem4  7753  fin1a2lem10  8035  uzwo  10281  seqf1olem1  11085  seqf1olem2  11086  hashnncl  11354  pceq0  12923  vdwmc2  13026  odcau  14915  dprdsn  15271  islss  15692  fidomndrnglem  16047  mvrf1  16170  obs2ss  16629  obslbs  16630  regr1lem2  17431  iccpnfhmeo  18443  itg10a  19065  dvlip  19340  mpfrcl  19402  deg1ge  19484  elply2  19578  coeeulem  19606  dgrle  19625  coemullem  19631  basellem2  20319  perfectlem2  20469  lgsabs1  20573  lnon0  21376  atsseq  22927  suppss2f  23201  cvmseu  23807  uninqs  25039  cbcpcp  25162  dsmmacl  27207  lsatcmp  29193  lsatcmp2  29194  ltrnnid  30325  trlatn0  30361  cdlemh  31006  dochlkr  31575
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 2448
  Copyright terms: Public domain W3C validator