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

Theorem pm3.35 585
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 427 1  |-  ( (
ph  /\  ( ph  ->  ps ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ornld  896  r19.29af2OLD  2921  r19.29vva  2926  2reu5  3233  intab  4230  dfac5  8422  grothpw  9115  grothpwex  9116  gcdcllem1  14151  gsmsymgreqlem2  16573  neindisj2  19710  tx1stc  20236  ufinffr  20515  ucnima  20869  fmcncfil  28067  sgn3da  28663  itg2gt0cn  30236  unirep  30369  ispridl2  30601  cnf1dd  30656  impel  30669  fmul01  31740  dvnmptconst  31904  dvnmul  31906  unisnALT  34073  ax6e2ndALT  34077  bnj605  34312  bnj594  34317  bnj1174  34406
  Copyright terms: Public domain W3C validator