Theorem pm3.35 801

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ornld  1060  2reu5  3719  intab  4944  dfac5  10073  grothpw  10771  grothpwex  10772  gcdcllem1  16390  gsmsymgreqlem2  19227  neindisj2  22511  tx1stc  23038  ufinffr  23317  ucnima  23670  frgr2wwlk1  29336  r19.29ffa  31465  prmidl2  32289  fmcncfil  32601  sgn3da  33230  bnj605  33608  bnj594  33613  bnj1174  33704  itg2gt0cn  36206  unirep  36245  ispridl2  36570  cnf1dd  36622  faosnf0.11b  41821  dfsucon  41917  unisnALT  43330  ax6e2ndALT  43334  ssinc  43419  ssdec  43420  fmul01  43941  dvnmptconst  44302  dvnmul  44304  2reu8i  45465  iccpartnel  45750  stgoldbwt  46088  sbgoldbalt  46093  bgoldbtbnd  46121