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

Theorem pm3.35 572
Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
Assertion
Ref Expression
pm3.35  |-  ( (
ph  /\  ( ph  ->  ps ) )  ->  ps )

Proof of Theorem pm3.35
StepHypRef Expression
1 pm2.27 37 . 2  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
21imp 420 1  |-  ( (
ph  /\  ( ph  ->  ps ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360
This theorem is referenced by:  2reu5  2975  intab  3894  dfac5  7751  grothpw  8444  grothpwex  8445  gcdcllem1  12685  neindisj2  16855  tx1stc  17339  ufinffr  17619  cmptdst  24968  unirep  25749  ispridl2  26063  fmul01  27110  climsuselem1  27133  stoweidlem3  27152  unisnALT  27971  notnot2ALT2  27972  a9e2ndALT  27976  bnj605  28207  bnj594  28212  bnj1174  28301
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator