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  2973  intab  3892  dfac5  7755  grothpw  8448  grothpwex  8449  gcdcllem1  12690  neindisj2  16860  tx1stc  17344  ufinffr  17624  cmptdst  25568  unirep  26349  ispridl2  26663  fmul01  27710  climsuselem1  27733  stoweidlem3  27752  unisnALT  28702  notnot2ALT2  28703  a9e2ndALT  28707  bnj605  28939  bnj594  28944  bnj1174  29033
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