Theorem pm3.35 802

Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. Variant of pm2.27 42. (Contributed by NM, 14-Dec-2002.)

Assertion

Ref	Expression
pm3.35	⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Proof of Theorem pm3.35

Step	Hyp	Ref	Expression
1		pm2.27 42	. 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	imp 406	1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ornld  1061  2reu5  3741  intab  4954  dfac5  10143  grothpw  10840  grothpwex  10841  gcdcllem1  16518  gsmsymgreqlem2  19412  neindisj2  23061  tx1stc  23588  ufinffr  23867  ucnima  24219  frgr2wwlk1  30310  r19.29ffa  32452  sgn3da  32813  prmidl2  33456  fmcncfil  33962  bnj605  34938  bnj594  34943  bnj1174  35034  itg2gt0cn  37699  unirep  37738  ispridl2  38062  cnf1dd  38114  faosnf0.11b  43451  dfsucon  43547  unisnALT  44950  ax6e2ndALT  44954  ssinc  45111  ssdec  45112  fmul01  45609  dvnmptconst  45970  dvnmul  45972  2reu8i  47142  iccpartnel  47452  stgoldbwt  47790  sbgoldbalt  47795  bgoldbtbnd  47823