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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ornld  1057  2reu5  3697  intab  4868  dfac5  9539  grothpw  10237  grothpwex  10238  gcdcllem1  15838  gsmsymgreqlem2  18551  neindisj2  21728  tx1stc  22255  ufinffr  22534  ucnima  22887  frgr2wwlk1  28114  r19.29ffa  30244  prmidl2  31024  fmcncfil  31284  sgn3da  31909  bnj605  32289  bnj594  32294  bnj1174  32385  itg2gt0cn  35112  unirep  35151  ispridl2  35476  cnf1dd  35528  dfsucon  40231  unisnALT  41632  ax6e2ndALT  41636  ssinc  41723  ssdec  41724  fmul01  42222  dvnmptconst  42583  dvnmul  42585  2reu8i  43669  iccpartnel  43955  stgoldbwt  44294  sbgoldbalt  44299  bgoldbtbnd  44327