Theorem pm3.35 838

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

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  ornld  1085  r19.29vva  3263  2reu5  3615  intab  4698  dfac5  9238  grothpw  9937  grothpwex  9938  gcdcllem1  15555  gsmsymgreqlem2  18162  neindisj2  21255  tx1stc  21781  ufinffr  22060  ucnima  22412  frgr2wwlk1  27677  r19.29ffa  29844  fmcncfil  30492  sgn3da  31119  bnj605  31493  bnj594  31498  bnj1174  31587  bj-ssbequ2  33148  itg2gt0cn  33952  unirep  33994  ispridl2  34323  cnf1dd  34378  unisnALT  39917  ax6e2ndALT  39921  ssinc  40018  ssdec  40019  fmul01  40551  dvnmptconst  40895  dvnmul  40897  iccpartnel  42209  stgoldbwt  42441  sbgoldbalt  42446  bgoldbtbnd  42474