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 610
Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
Assertion
Ref Expression
pm3.35 ((𝜑 ∧ (𝜑𝜓)) → 𝜓)

Proof of Theorem pm3.35
StepHypRef Expression
1 pm2.27 42 . 2 (𝜑 → ((𝜑𝜓) → 𝜓))
21imp 445 1 ((𝜑 ∧ (𝜑𝜓)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  ornld  939  r19.29vva  3073  2reu5  3398  intab  4472  dfac5  8895  grothpw  9592  grothpwex  9593  gcdcllem1  15145  gsmsymgreqlem2  17772  neindisj2  20837  tx1stc  21363  ufinffr  21643  ucnima  21995  fmcncfil  29756  sgn3da  30381  bnj605  30682  bnj594  30687  bnj1174  30776  bj-ssbequ2  32282  itg2gt0cn  33094  unirep  33136  ispridl2  33466  cnf1dd  33521  unisnALT  38642  ax6e2ndALT  38646  ssinc  38746  ssdec  38747  fmul01  39213  dvnmptconst  39459  dvnmul  39461  iccpartnel  40669  stgoldbwt  40956  sgoldbalt  40961  bgoldbtbnd  40983
  Copyright terms: Public domain W3C validator