Theorem pm3.35 803

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  3766  intab  4982  dfac5  10166  grothpw  10863  grothpwex  10864  gcdcllem1  16532  gsmsymgreqlem2  19463  neindisj2  23146  tx1stc  23673  ufinffr  23952  ucnima  24305  frgr2wwlk1  30357  r19.29ffa  32499  prmidl2  33448  fmcncfil  33891  sgn3da  34522  bnj605  34899  bnj594  34904  bnj1174  34995  itg2gt0cn  37661  unirep  37700  ispridl2  38024  cnf1dd  38076  faosnf0.11b  43416  dfsucon  43512  unisnALT  44923  ax6e2ndALT  44927  ssinc  45026  ssdec  45027  fmul01  45535  dvnmptconst  45896  dvnmul  45898  2reu8i  47062  iccpartnel  47362  stgoldbwt  47700  sbgoldbalt  47705  bgoldbtbnd  47733