Theorem pm3.35 799

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 206  df-an 396

This theorem is referenced by:  ornld  1058  2reu5  3688  intab  4906  dfac5  9815  grothpw  10513  grothpwex  10514  gcdcllem1  16134  gsmsymgreqlem2  18954  neindisj2  22182  tx1stc  22709  ufinffr  22988  ucnima  23341  frgr2wwlk1  28594  r19.29ffa  30723  prmidl2  31518  fmcncfil  31783  sgn3da  32408  bnj605  32787  bnj594  32792  bnj1174  32883  itg2gt0cn  35759  unirep  35798  ispridl2  36123  cnf1dd  36175  dfsucon  41028  unisnALT  42435  ax6e2ndALT  42439  ssinc  42526  ssdec  42527  fmul01  43011  dvnmptconst  43372  dvnmul  43374  2reu8i  44492  iccpartnel  44778  stgoldbwt  45116  sbgoldbalt  45121  bgoldbtbnd  45149