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  3713  intab  4928  dfac5  10027  grothpw  10724  grothpwex  10725  gcdcllem1  16412  gsmsymgreqlem2  19345  neindisj2  23039  tx1stc  23566  ufinffr  23845  ucnima  24196  frgr2wwlk1  30311  r19.29ffa  32452  sgn3da  32822  prmidl2  33413  fmcncfil  33965  bnj605  34940  bnj594  34945  bnj1174  35036  itg2gt0cn  37735  unirep  37774  ispridl2  38098  cnf1dd  38150  faosnf0.11b  43544  dfsucon  43640  unisnALT  45042  ax6e2ndALT  45046  ssinc  45208  ssdec  45209  fmul01  45704  dvnmptconst  46063  dvnmul  46065  2reu8i  47237  iccpartnel  47562  stgoldbwt  47900  sbgoldbalt  47905  bgoldbtbnd  47933