Theorem pm3.35 801

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 409	1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ornld  1056  r19.29vvaOLD  3337  2reu5  3749  intab  4899  dfac5  9548  grothpw  10242  grothpwex  10243  gcdcllem1  15842  gsmsymgreqlem2  18553  neindisj2  21725  tx1stc  22252  ufinffr  22531  ucnima  22884  frgr2wwlk1  28102  r19.29ffa  30231  prmidl2  30953  fmcncfil  31169  sgn3da  31794  bnj605  32174  bnj594  32179  bnj1174  32270  itg2gt0cn  34941  unirep  34982  ispridl2  35310  cnf1dd  35362  dfsucon  39882  unisnALT  41253  ax6e2ndALT  41257  ssinc  41346  ssdec  41347  fmul01  41853  dvnmptconst  42218  dvnmul  42220  2reu8i  43305  iccpartnel  43591  stgoldbwt  43934  sbgoldbalt  43939  bgoldbtbnd  43967