Theorem pm3.35 611

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

Step	Hyp	Ref	Expression
1		pm2.27 42	. 2 |- ( ph -> ( ( ph -> ps ) -> ps ) )
2	1	imp 445	1 |- ( ( ph /\ ( ph -> ps ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  ornld  940  r19.29vva  3081  2reu5  3416  intab  4507  dfac5  8951  grothpw  9648  grothpwex  9649  gcdcllem1  15221  gsmsymgreqlem2  17851  neindisj2  20927  tx1stc  21453  ufinffr  21733  ucnima  22085  frgr2wwlk1  27193  r19.29ffa  29320  fmcncfil  29977  sgn3da  30603  bnj605  30977  bnj594  30982  bnj1174  31071  bj-ssbequ2  32643  itg2gt0cn  33465  unirep  33507  ispridl2  33837  cnf1dd  33892  unisnALT  39162  ax6e2ndALT  39166  ssinc  39264  ssdec  39265  fmul01  39812  dvnmptconst  40156  dvnmul  40158  iccpartnel  41374  stgoldbwt  41664  sbgoldbalt  41669  bgoldbtbnd  41697