Theorem pm3.35 815

Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. Variant of pm2.27 43. (Contributed by NM, 14-Dec-2002.)

Assertion

Ref	Expression
pm3.35	⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Proof of Theorem pm3.35

Step	Hyp	Ref	Expression
1		pm2.27 43	. 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	imp 412	1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ornld  1077  2reu5  3716  intab  4938  dfac5  10188  grothpw  10892  grothpwex  10893  sgn3da  15234  gcdcllem1  16649  gsmsymgreqlem2  19625  prmidl2  21602  neindisj2  23421  tx1stc  23949  ufinffr  24228  ucnima  24579  frgr2wwlk1  30912  r19.29ffa  33050  fmcncfil  34545  bnj605  35520  bnj594  35525  bnj1174  35616  bj-cbvew  37511  itg2gt0cn  38561  unirep  38616  ispridl2  38940  cnf1dd  38990  faosnf0.11b  44386  dfsucon  44482  unisnALT  45867  ax6e2ndALT  45871  ssinc  46045  ssdec  46046  fmul01  46536  dvnmptconst  46895  dvnmul  46897  2reu8i  48127  iccpartnel  48464  stgoldbwt  48818  sbgoldbalt  48823  bgoldbtbnd  48851