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 838
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 396 1 ((𝜑 ∧ (𝜑𝜓)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  ornld  1085  r19.29vva  3263  2reu5  3615  intab  4698  dfac5  9238  grothpw  9937  grothpwex  9938  gcdcllem1  15555  gsmsymgreqlem2  18162  neindisj2  21255  tx1stc  21781  ufinffr  22060  ucnima  22412  frgr2wwlk1  27677  r19.29ffa  29844  fmcncfil  30492  sgn3da  31119  bnj605  31493  bnj594  31498  bnj1174  31587  bj-ssbequ2  33148  itg2gt0cn  33952  unirep  33994  ispridl2  34323  cnf1dd  34378  unisnALT  39917  ax6e2ndALT  39921  ssinc  40018  ssdec  40019  fmul01  40551  dvnmptconst  40895  dvnmul  40897  iccpartnel  42209  stgoldbwt  42441  sbgoldbalt  42446  bgoldbtbnd  42474
  Copyright terms: Public domain W3C validator