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  3732  intab  4945  dfac5  10089  grothpw  10786  grothpwex  10787  gcdcllem1  16476  gsmsymgreqlem2  19368  neindisj2  23017  tx1stc  23544  ufinffr  23823  ucnima  24175  frgr2wwlk1  30265  r19.29ffa  32407  sgn3da  32766  prmidl2  33419  fmcncfil  33928  bnj605  34904  bnj594  34909  bnj1174  35000  itg2gt0cn  37676  unirep  37715  ispridl2  38039  cnf1dd  38091  faosnf0.11b  43423  dfsucon  43519  unisnALT  44922  ax6e2ndALT  44926  ssinc  45088  ssdec  45089  fmul01  45585  dvnmptconst  45946  dvnmul  45948  2reu8i  47118  iccpartnel  47443  stgoldbwt  47781  sbgoldbalt  47786  bgoldbtbnd  47814