MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.35 Structured version   Visualization version   GIF version

Theorem pm3.35 799
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
StepHypRef Expression
1 pm2.27 42 . 2 (𝜑 → ((𝜑𝜓) → 𝜓))
21imp 406 1 ((𝜑 ∧ (𝜑𝜓)) → 𝜓)
Colors of variables: wff setvar class
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 206  df-an 396
This theorem is referenced by:  ornld  1058  2reu5  3696  intab  4914  dfac5  9868  grothpw  10566  grothpwex  10567  gcdcllem1  16187  gsmsymgreqlem2  19020  neindisj2  22255  tx1stc  22782  ufinffr  23061  ucnima  23414  frgr2wwlk1  28672  r19.29ffa  30801  prmidl2  31595  fmcncfil  31860  sgn3da  32487  bnj605  32866  bnj594  32871  bnj1174  32962  itg2gt0cn  35811  unirep  35850  ispridl2  36175  cnf1dd  36227  dfsucon  41092  unisnALT  42499  ax6e2ndALT  42503  ssinc  42590  ssdec  42591  fmul01  43075  dvnmptconst  43436  dvnmul  43438  2reu8i  44556  iccpartnel  44842  stgoldbwt  45180  sbgoldbalt  45185  bgoldbtbnd  45213
  Copyright terms: Public domain W3C validator