Theorem pm3.35 609

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 41	. 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	imp 444	1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ornld  938  r19.29vva  3062  2reu5  3383  intab  4442  dfac5  8834  grothpw  9527  grothpwex  9528  gcdcllem1  15059  gsmsymgreqlem2  17674  neindisj2  20737  tx1stc  21263  ufinffr  21543  ucnima  21895  fmcncfil  29305  sgn3da  29930  bnj605  30231  bnj594  30236  bnj1174  30325  bj-ssbequ2  31832  itg2gt0cn  32635  unirep  32677  ispridl2  33007  cnf1dd  33062  unisnALT  38184  ax6e2ndALT  38188  ssinc  38292  ssdec  38293  fmul01  38647  dvnmptconst  38831  dvnmul  38833  iccpartnel  39976  stgoldbwt  40198  sgoldbalt  40203  bgoldbtbnd  40225