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  3764  intab  4978  dfac5  10169  grothpw  10866  grothpwex  10867  gcdcllem1  16536  gsmsymgreqlem2  19449  neindisj2  23131  tx1stc  23658  ufinffr  23937  ucnima  24290  frgr2wwlk1  30348  r19.29ffa  32490  prmidl2  33469  fmcncfil  33930  sgn3da  34544  bnj605  34921  bnj594  34926  bnj1174  35017  itg2gt0cn  37682  unirep  37721  ispridl2  38045  cnf1dd  38097  faosnf0.11b  43440  dfsucon  43536  unisnALT  44946  ax6e2ndALT  44950  ssinc  45092  ssdec  45093  fmul01  45595  dvnmptconst  45956  dvnmul  45958  2reu8i  47125  iccpartnel  47425  stgoldbwt  47763  sbgoldbalt  47768  bgoldbtbnd  47796