Theorem pm3.35 800

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ornld  1059  2reu5  3693  intab  4909  dfac5  9884  grothpw  10582  grothpwex  10583  gcdcllem1  16206  gsmsymgreqlem2  19039  neindisj2  22274  tx1stc  22801  ufinffr  23080  ucnima  23433  frgr2wwlk1  28693  r19.29ffa  30822  prmidl2  31616  fmcncfil  31881  sgn3da  32508  bnj605  32887  bnj594  32892  bnj1174  32983  itg2gt0cn  35832  unirep  35871  ispridl2  36196  cnf1dd  36248  dfsucon  41130  unisnALT  42546  ax6e2ndALT  42550  ssinc  42637  ssdec  42638  fmul01  43121  dvnmptconst  43482  dvnmul  43484  2reu8i  44605  iccpartnel  44890  stgoldbwt  45228  sbgoldbalt  45233  bgoldbtbnd  45261