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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  ornld  1061  2reu5  3755  intab  4983  dfac5  10123  grothpw  10821  grothpwex  10822  gcdcllem1  16440  gsmsymgreqlem2  19299  neindisj2  22627  tx1stc  23154  ufinffr  23433  ucnima  23786  frgr2wwlk1  29582  r19.29ffa  31713  prmidl2  32559  fmcncfil  32911  sgn3da  33540  bnj605  33918  bnj594  33923  bnj1174  34014  itg2gt0cn  36543  unirep  36582  ispridl2  36906  cnf1dd  36958  faosnf0.11b  42178  dfsucon  42274  unisnALT  43687  ax6e2ndALT  43691  ssinc  43776  ssdec  43777  fmul01  44296  dvnmptconst  44657  dvnmul  44659  2reu8i  45821  iccpartnel  46106  stgoldbwt  46444  sbgoldbalt  46449  bgoldbtbnd  46477