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  3716  intab  4933  dfac5  10039  grothpw  10737  grothpwex  10738  gcdcllem1  16426  gsmsymgreqlem2  19360  neindisj2  23067  tx1stc  23594  ufinffr  23873  ucnima  24224  frgr2wwlk1  30404  r19.29ffa  32545  sgn3da  32915  prmidl2  33522  fmcncfil  34088  bnj605  35063  bnj594  35068  bnj1174  35159  itg2gt0cn  37872  unirep  37911  ispridl2  38235  cnf1dd  38287  faosnf0.11b  43664  dfsucon  43760  unisnALT  45162  ax6e2ndALT  45166  ssinc  45327  ssdec  45328  fmul01  45822  dvnmptconst  46181  dvnmul  46183  2reu8i  47355  iccpartnel  47680  stgoldbwt  48018  sbgoldbalt  48023  bgoldbtbnd  48051