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  3720  intab  4931  dfac5  10042  grothpw  10739  grothpwex  10740  gcdcllem1  16428  gsmsymgreqlem2  19328  neindisj2  23026  tx1stc  23553  ufinffr  23832  ucnima  24184  frgr2wwlk1  30291  r19.29ffa  32433  sgn3da  32792  prmidl2  33388  fmcncfil  33897  bnj605  34873  bnj594  34878  bnj1174  34969  itg2gt0cn  37654  unirep  37693  ispridl2  38017  cnf1dd  38069  faosnf0.11b  43400  dfsucon  43496  unisnALT  44899  ax6e2ndALT  44903  ssinc  45065  ssdec  45066  fmul01  45562  dvnmptconst  45923  dvnmul  45925  2reu8i  47098  iccpartnel  47423  stgoldbwt  47761  sbgoldbalt  47766  bgoldbtbnd  47794