Theorem pm3.35 802

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  3780  intab  5002  dfac5  10198  grothpw  10895  grothpwex  10896  gcdcllem1  16545  gsmsymgreqlem2  19473  neindisj2  23152  tx1stc  23679  ufinffr  23958  ucnima  24311  frgr2wwlk1  30361  r19.29ffa  32500  prmidl2  33434  fmcncfil  33877  sgn3da  34506  bnj605  34883  bnj594  34888  bnj1174  34979  itg2gt0cn  37635  unirep  37674  ispridl2  37998  cnf1dd  38050  faosnf0.11b  43389  dfsucon  43485  unisnALT  44897  ax6e2ndALT  44901  ssinc  44989  ssdec  44990  fmul01  45501  dvnmptconst  45862  dvnmul  45864  2reu8i  47028  iccpartnel  47312  stgoldbwt  47650  sbgoldbalt  47655  bgoldbtbnd  47683