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:  ornld  896  r19.29af2  3005  r19.29_2a  3010  2reu5  3317  intab  4318  dfac5  8521  grothpw  9216  grothpwex  9217  gcdcllem1  14025  gsmsymgreqlem2  16328  neindisj2  19492  tx1stc  20019  ufinffr  20298  ucnima  20652  tgldim0eq  23760  fmcncfil  27738  sgn3da  28305  itg2gt0cn  29997  unirep  30130  ispridl2  30362  cnf1dd  30417  impel  30430  fmul01  31453  iblspltprt  31614  itgspltprt  31620  unisnALT  33207  ax6e2ndALT  33211  bnj605  33445  bnj594  33450  bnj1174  33539
  Copyright terms: Public domain W3C validator