Theorem pm3.35 808

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

This theorem is referenced by:  ornld  1067  2reu5  3706  intab  4915  dfac5  10049  grothpw  10747  grothpwex  10748  gcdcllem1  16466  gsmsymgreqlem2  19404  neindisj2  23113  tx1stc  23640  ufinffr  23919  ucnima  24270  frgr2wwlk1  30424  r19.29ffa  32565  sgn3da  32933  prmidl2  33531  fmcncfil  34122  bnj605  35096  bnj594  35101  bnj1174  35192  bj-cbvew  36989  itg2gt0cn  38049  unirep  38088  ispridl2  38412  cnf1dd  38464  faosnf0.11b  43878  dfsucon  43974  unisnALT  45376  ax6e2ndALT  45380  ssinc  45541  ssdec  45542  fmul01  46032  dvnmptconst  46391  dvnmul  46393  2reu8i  47583  iccpartnel  47920  stgoldbwt  48274  sbgoldbalt  48279  bgoldbtbnd  48307