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

Theorem pm3.35 587
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 39 . 2  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
21imp 429 1  |-  ( (
ph  /\  ( ph  ->  ps ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  r19.29af2  2881  r19.29_2a  2885  2reu5  3188  intab  4179  dfac5  8319  grothpw  9014  grothpwex  9015  gcdcllem1  13716  gsmsymgreqlem2  15957  neindisj2  18749  tx1stc  19245  ufinffr  19524  ucnima  19878  tgldim0eq  22978  fmcncfil  26383  sgn3da  26946  itg2gt0cn  28473  unirep  28632  ispridl2  28864  cnf1dd  28919  impel  28932  fmul01  29787  ccats1rev  30286  unisnALT  31758  ax6e2ndALT  31762  bnj605  31996  bnj594  32001  bnj1174  32090
  Copyright terms: Public domain W3C validator