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  3717  intab  4928  dfac5  10017  grothpw  10714  grothpwex  10715  gcdcllem1  16407  gsmsymgreqlem2  19341  neindisj2  23036  tx1stc  23563  ufinffr  23842  ucnima  24193  frgr2wwlk1  30304  r19.29ffa  32445  sgn3da  32812  prmidl2  33401  fmcncfil  33939  bnj605  34914  bnj594  34919  bnj1174  35010  itg2gt0cn  37714  unirep  37753  ispridl2  38077  cnf1dd  38129  faosnf0.11b  43459  dfsucon  43555  unisnALT  44957  ax6e2ndALT  44961  ssinc  45123  ssdec  45124  fmul01  45619  dvnmptconst  45978  dvnmul  45980  2reu8i  47143  iccpartnel  47468  stgoldbwt  47806  sbgoldbalt  47811  bgoldbtbnd  47839