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  10135  grothpw  10839  grothpwex  10840  sgn3da  15178  gcdcllem1  16595  gsmsymgreqlem2  19564  prmidl2  21535  neindisj2  23354  tx1stc  23882  ufinffr  24161  ucnima  24512  frgr2wwlk1  30817  r19.29ffa  32955  fmcncfil  34449  bnj605  35424  bnj594  35429  bnj1174  35520  bj-cbvew  37380  itg2gt0cn  38432  unirep  38472  ispridl2  38796  cnf1dd  38846  faosnf0.11b  44275  dfsucon  44371  unisnALT  45756  ax6e2ndALT  45760  ssinc  45927  ssdec  45928  fmul01  46418  dvnmptconst  46777  dvnmul  46779  2reu8i  48009  iccpartnel  48346  stgoldbwt  48700  sbgoldbalt  48705  bgoldbtbnd  48733