Theorem pm3.35 802

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  1061  2reu5  3729  intab  4942  dfac5  10082  grothpw  10779  grothpwex  10780  gcdcllem1  16469  gsmsymgreqlem2  19361  neindisj2  23010  tx1stc  23537  ufinffr  23816  ucnima  24168  frgr2wwlk1  30258  r19.29ffa  32400  sgn3da  32759  prmidl2  33412  fmcncfil  33921  bnj605  34897  bnj594  34902  bnj1174  34993  itg2gt0cn  37669  unirep  37708  ispridl2  38032  cnf1dd  38084  faosnf0.11b  43416  dfsucon  43512  unisnALT  44915  ax6e2ndALT  44919  ssinc  45081  ssdec  45082  fmul01  45578  dvnmptconst  45939  dvnmul  45941  2reu8i  47114  iccpartnel  47439  stgoldbwt  47777  sbgoldbalt  47782  bgoldbtbnd  47810