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

Theorem pm3.35 573
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:  intab  3833  dfac5  7688  grothpw  8381  grothpwex  8382  gcdcllem1  12617  neindisj2  16787  2ndcdisj  17109  tx1stc  17271  ufinffr  17551  cmptdst  24900  unirep  25681  ispridl2  25995  fmul01  27043  stoweidlem3  27052  unisnALT  27715  notnot2ALT2  27716  a9e2ndALT  27720  bnj605  27951  bnj594  27956  bnj1174  28045
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