Theorem pm3.35 815

Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. Variant of pm2.27 43. (Contributed by NM, 14-Dec-2002.)

Assertion

Ref	Expression
pm3.35	⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

Proof of Theorem pm3.35

Step	Hyp	Ref	Expression
1		pm2.27 43	. 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	imp 412	1 ⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ornld  1077  2reu5  3724  intab  4948  dfac5  10131  grothpw  10829  grothpwex  10830  sgn3da  15164  gcdcllem1  16582  gsmsymgreqlem2  19532  prmidl2  21503  neindisj2  23317  tx1stc  23844  ufinffr  24123  ucnima  24474  frgr2wwlk1  30717  r19.29ffa  32855  fmcncfil  34352  bnj605  35327  bnj594  35332  bnj1174  35423  bj-cbvew  37305  itg2gt0cn  38367  unirep  38406  ispridl2  38730  cnf1dd  38780  faosnf0.11b  44194  dfsucon  44290  unisnALT  45675  ax6e2ndALT  45679  ssinc  45846  ssdec  45847  fmul01  46337  dvnmptconst  46696  dvnmul  46698  2reu8i  47891  iccpartnel  48228  stgoldbwt  48582  sbgoldbalt  48587  bgoldbtbnd  48615