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 408	1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ornld  1061  2reu5  3755  intab  4983  dfac5  10123  grothpw  10821  grothpwex  10822  gcdcllem1  16440  gsmsymgreqlem2  19299  neindisj2  22627  tx1stc  23154  ufinffr  23433  ucnima  23786  frgr2wwlk1  29613  r19.29ffa  31744  prmidl2  32590  fmcncfil  32942  sgn3da  33571  bnj605  33949  bnj594  33954  bnj1174  34045  itg2gt0cn  36591  unirep  36630  ispridl2  36954  cnf1dd  37006  faosnf0.11b  42226  dfsucon  42322  unisnALT  43735  ax6e2ndALT  43739  ssinc  43824  ssdec  43825  fmul01  44344  dvnmptconst  44705  dvnmul  44707  2reu8i  45869  iccpartnel  46154  stgoldbwt  46492  sbgoldbalt  46497  bgoldbtbnd  46525