Theorem pm3.35 812

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ornld  1072  2reu5  3720  intab  4935  dfac5  10082  grothpw  10781  grothpwex  10782  gcdcllem1  16516  gsmsymgreqlem2  19454  neindisj2  23163  tx1stc  23690  ufinffr  23969  ucnima  24320  frgr2wwlk1  30477  r19.29ffa  32618  sgn3da  32986  prmidl2  33588  fmcncfil  34189  bnj605  35166  bnj594  35171  bnj1174  35262  bj-cbvew  37078  itg2gt0cn  38138  unirep  38177  ispridl2  38501  cnf1dd  38553  faosnf0.11b  43967  dfsucon  44063  unisnALT  45465  ax6e2ndALT  45469  ssinc  45629  ssdec  45630  fmul01  46120  dvnmptconst  46479  dvnmul  46481  2reu8i  47671  iccpartnel  48008  stgoldbwt  48362  sbgoldbalt  48367  bgoldbtbnd  48395