Theorem pm3.35 803

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ornld  1062  2reu5  3705  intab  4921  dfac5  10042  grothpw  10740  grothpwex  10741  gcdcllem1  16459  gsmsymgreqlem2  19397  neindisj2  23098  tx1stc  23625  ufinffr  23904  ucnima  24255  frgr2wwlk1  30414  r19.29ffa  32555  sgn3da  32922  prmidl2  33516  fmcncfil  34091  bnj605  35065  bnj594  35070  bnj1174  35161  bj-cbvew  36952  itg2gt0cn  38010  unirep  38049  ispridl2  38373  cnf1dd  38425  faosnf0.11b  43872  dfsucon  43968  unisnALT  45370  ax6e2ndALT  45374  ssinc  45535  ssdec  45536  fmul01  46028  dvnmptconst  46387  dvnmul  46389  2reu8i  47573  iccpartnel  47910  stgoldbwt  48264  sbgoldbalt  48269  bgoldbtbnd  48297