Theorem pm3.35 803

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ornld  1062  2reu5  3718  intab  4935  dfac5  10051  grothpw  10749  grothpwex  10750  gcdcllem1  16438  gsmsymgreqlem2  19372  neindisj2  23079  tx1stc  23606  ufinffr  23885  ucnima  24236  frgr2wwlk1  30416  r19.29ffa  32556  sgn3da  32925  prmidl2  33533  fmcncfil  34108  bnj605  35082  bnj594  35087  bnj1174  35178  bj-cbvew  36879  itg2gt0cn  37920  unirep  37959  ispridl2  38283  cnf1dd  38335  faosnf0.11b  43777  dfsucon  43873  unisnALT  45275  ax6e2ndALT  45279  ssinc  45440  ssdec  45441  fmul01  45934  dvnmptconst  46293  dvnmul  46295  2reu8i  47467  iccpartnel  47792  stgoldbwt  48130  sbgoldbalt  48135  bgoldbtbnd  48163