Theorem pm3.35 814

Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. Variant of pm2.27 43. (Contributed by NM, 14-Dec-2002.)

Assertion

Ref	Expression
pm3.35	⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Proof of Theorem pm3.35

Step	Hyp	Ref	Expression
1		pm2.27 43	. 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	imp 411	1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ornld  1077  2reu5  3722  intab  4944  dfac5  10113  grothpw  10812  grothpwex  10813  sgn3da  15140  gcdcllem1  16558  gsmsymgreqlem2  19502  prmidl2  21447  neindisj2  23261  tx1stc  23788  ufinffr  24067  ucnima  24418  frgr2wwlk1  30658  r19.29ffa  32796  fmcncfil  34299  bnj605  35273  bnj594  35278  bnj1174  35369  bj-cbvew  37242  itg2gt0cn  38304  unirep  38343  ispridl2  38667  cnf1dd  38717  faosnf0.11b  44133  dfsucon  44229  unisnALT  45614  ax6e2ndALT  45618  ssinc  45785  ssdec  45786  fmul01  46276  dvnmptconst  46635  dvnmul  46637  2reu8i  47827  iccpartnel  48164  stgoldbwt  48518  sbgoldbalt  48523  bgoldbtbnd  48551