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 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
StepHypRef Expression
1 pm2.27 42 . 2 (𝜑 → ((𝜑𝜓) → 𝜓))
21imp 410 1 ((𝜑 ∧ (𝜑𝜓)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ornld  1057  r19.29vvaOLD  3322  2reu5  3726  intab  4879  dfac5  9531  grothpw  10225  grothpwex  10226  gcdcllem1  15825  gsmsymgreqlem2  18537  neindisj2  21706  tx1stc  22233  ufinffr  22512  ucnima  22865  frgr2wwlk1  28092  r19.29ffa  30221  prmidl2  30967  fmcncfil  31181  sgn3da  31806  bnj605  32186  bnj594  32191  bnj1174  32282  itg2gt0cn  34992  unirep  35031  ispridl2  35356  cnf1dd  35408  dfsucon  40028  unisnALT  41417  ax6e2ndALT  41421  ssinc  41510  ssdec  41511  fmul01  42015  dvnmptconst  42376  dvnmul  42378  2reu8i  43462  iccpartnel  43748  stgoldbwt  44088  sbgoldbalt  44093  bgoldbtbnd  44121
  Copyright terms: Public domain W3C validator