Theorem pm3.35 803

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  1062  2reu5  3705  intab  4921  dfac5  10040  grothpw  10738  grothpwex  10739  gcdcllem1  16457  gsmsymgreqlem2  19395  neindisj2  23096  tx1stc  23623  ufinffr  23902  ucnima  24253  frgr2wwlk1  30412  r19.29ffa  32553  sgn3da  32920  prmidl2  33514  fmcncfil  34089  bnj605  35063  bnj594  35068  bnj1174  35159  bj-cbvew  36942  itg2gt0cn  38000  unirep  38039  ispridl2  38363  cnf1dd  38415  faosnf0.11b  43862  dfsucon  43958  unisnALT  45360  ax6e2ndALT  45364  ssinc  45525  ssdec  45526  fmul01  46018  dvnmptconst  46377  dvnmul  46379  2reu8i  47563  iccpartnel  47900  stgoldbwt  48254  sbgoldbalt  48259  bgoldbtbnd  48287