Theorem pm3.35 799

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

This theorem is referenced by:  ornld  1058  2reu5  3696  intab  4914  dfac5  9868  grothpw  10566  grothpwex  10567  gcdcllem1  16187  gsmsymgreqlem2  19020  neindisj2  22255  tx1stc  22782  ufinffr  23061  ucnima  23414  frgr2wwlk1  28672  r19.29ffa  30801  prmidl2  31595  fmcncfil  31860  sgn3da  32487  bnj605  32866  bnj594  32871  bnj1174  32962  itg2gt0cn  35811  unirep  35850  ispridl2  36175  cnf1dd  36227  dfsucon  41092  unisnALT  42499  ax6e2ndALT  42503  ssinc  42590  ssdec  42591  fmul01  43075  dvnmptconst  43436  dvnmul  43438  2reu8i  44556  iccpartnel  44842  stgoldbwt  45180  sbgoldbalt  45185  bgoldbtbnd  45213