Theorem pm3.35 610

Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (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 445	1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  ornld  939  r19.29vva  3075  2reu5  3403  intab  4479  dfac5  8911  grothpw  9608  grothpwex  9609  gcdcllem1  15164  gsmsymgreqlem2  17791  neindisj2  20867  tx1stc  21393  ufinffr  21673  ucnima  22025  r19.29ffa  29208  fmcncfil  29801  sgn3da  30426  bnj605  30738  bnj594  30743  bnj1174  30832  bj-ssbequ2  32338  itg2gt0cn  33136  unirep  33178  ispridl2  33508  cnf1dd  33563  unisnALT  38684  ax6e2ndALT  38688  ssinc  38786  ssdec  38787  fmul01  39248  dvnmptconst  39493  dvnmul  39495  iccpartnel  40702  stgoldbwt  40989  sgoldbalt  40994  bgoldbtbnd  41016