Theorem pm3.35 815

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ornld  1077  2reu5  3715  intab  4937  dfac5  10210  grothpw  10914  grothpwex  10915  sgn3da  15259  gcdcllem1  16674  gsmsymgreqlem2  19650  prmidl2  21627  neindisj2  23446  tx1stc  23974  ufinffr  24253  ucnima  24604  frgr2wwlk1  30935  r19.29ffa  33115  fmcncfil  34609  bnj605  35583  bnj594  35588  bnj1174  35679  bj-cbvew  37633  itg2gt0cn  38686  unirep  38741  ispridl2  39065  cnf1dd  39115  faosnf0.11b  44521  dfsucon  44617  unisnALT  46001  ax6e2ndALT  46005  ssinc  46195  ssdec  46196  fmul01  46685  dvnmptconst  47044  dvnmul  47046  2reu8i  48276  iccpartnel  48613  stgoldbwt  48967  sbgoldbalt  48972  bgoldbtbnd  49000