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  1075  2reu5  3724  intab  4939  dfac5  10100  grothpw  10799  grothpwex  10800  sgn3da  15128  gcdcllem1  16547  gsmsymgreqlem2  19492  prmidl2  21428  neindisj2  23241  tx1stc  23768  ufinffr  24047  ucnima  24398  frgr2wwlk1  30589  r19.29ffa  32728  fmcncfil  34238  bnj605  35212  bnj594  35217  bnj1174  35308  bj-cbvew  37126  itg2gt0cn  38186  unirep  38225  ispridl2  38549  cnf1dd  38601  faosnf0.11b  44015  dfsucon  44111  unisnALT  45499  ax6e2ndALT  45503  ssinc  45663  ssdec  45664  fmul01  46154  dvnmptconst  46513  dvnmul  46515  2reu8i  47705  iccpartnel  48042  stgoldbwt  48396  sbgoldbalt  48401  bgoldbtbnd  48429