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

Theorem pm3.35 570
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 35 . 2  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
21imp 418 1  |-  ( (
ph  /\  ( ph  ->  ps ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  2reu5  2986  intab  3908  dfac5  7771  grothpw  8464  grothpwex  8465  gcdcllem1  12706  neindisj2  16876  tx1stc  17360  ufinffr  17640  itg2gt0cn  25006  cmptdst  25671  unirep  26452  ispridl2  26766  fmul01  27813  climsuselem1  27836  stoweidlem3  27855  unisnALT  29018  notnot2ALT2  29019  a9e2ndALT  29023  bnj605  29255  bnj594  29260  bnj1174  29349
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-an 360
  Copyright terms: Public domain W3C validator