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

Theorem pm3.35 571
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 419 1  |-  ( (
ph  /\  ( ph  ->  ps ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  r19.29af2  2835  r19.29_2a  2839  2reu5  3129  intab  4067  dfac5  7993  grothpw  8685  grothpwex  8686  gcdcllem1  12994  neindisj2  17170  tx1stc  17665  ufinffr  17944  ucnima  18294  fmcncfil  24300  itg2gt0cn  26201  unirep  26346  ispridl2  26580  fmul01  27619  unisnALT  28790  a9e2ndALT  28795  bnj605  29030  bnj594  29035  bnj1174  29124
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 178  df-an 361
  Copyright terms: Public domain W3C validator