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  1062  2reu5  3704  intab  4920  dfac5  10051  grothpw  10749  grothpwex  10750  gcdcllem1  16468  gsmsymgreqlem2  19406  neindisj2  23088  tx1stc  23615  ufinffr  23894  ucnima  24245  frgr2wwlk1  30399  r19.29ffa  32540  sgn3da  32907  prmidl2  33501  fmcncfil  34075  bnj605  35049  bnj594  35054  bnj1174  35145  bj-cbvew  36936  itg2gt0cn  37996  unirep  38035  ispridl2  38359  cnf1dd  38411  faosnf0.11b  43854  dfsucon  43950  unisnALT  45352  ax6e2ndALT  45356  ssinc  45517  ssdec  45518  fmul01  46010  dvnmptconst  46369  dvnmul  46371  2reu8i  47561  iccpartnel  47898  stgoldbwt  48252  sbgoldbalt  48257  bgoldbtbnd  48285