Theorem pm3.35 612

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

This theorem is referenced by:  ornld  976  r19.29vva  3217  2reu5  3555  intab  4657  dfac5  9139  grothpw  9838  grothpwex  9839  gcdcllem1  15421  gsmsymgreqlem2  18049  neindisj2  21127  tx1stc  21653  ufinffr  21932  ucnima  22284  frgr2wwlk1  27481  r19.29ffa  29627  fmcncfil  30284  sgn3da  30910  bnj605  31282  bnj594  31287  bnj1174  31376  bj-ssbequ2  32947  itg2gt0cn  33776  unirep  33818  ispridl2  34148  cnf1dd  34203  unisnALT  39659  ax6e2ndALT  39663  ssinc  39761  ssdec  39762  fmul01  40313  dvnmptconst  40657  dvnmul  40659  iccpartnel  41882  stgoldbwt  42172  sbgoldbalt  42177  bgoldbtbnd  42205