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  3719  intab  4941  dfac5  10234  grothpw  10938  grothpwex  10939  sgn3da  15283  gcdcllem1  16698  gsmsymgreqlem2  19675  prmidl2  21652  neindisj2  23471  tx1stc  23999  ufinffr  24278  ucnima  24629  frgr2wwlk1  30960  r19.29ffa  33140  fmcncfil  34633  bnj605  35607  bnj594  35612  bnj1174  35703  bj-cbvew  37719  itg2gt0cn  38785  unirep  38840  ispridl2  39164  cnf1dd  39214  faosnf0.11b  44620  dfsucon  44716  unisnALT  46099  ax6e2ndALT  46103  ssinc  46307  ssdec  46308  fmul01  46797  dvnmptconst  47156  dvnmul  47158  2reu8i  48389  iccpartnel  48725  stgoldbwt  49079  sbgoldbalt  49084  bgoldbtbnd  49112