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  3075  2reu5  3403  intab  4479  dfac5  8911  grothpw  9608  grothpwex  9609  gcdcllem1  15164  gsmsymgreqlem2  17791  neindisj2  20867  tx1stc  21393  ufinffr  21673  ucnima  22025  r19.29ffa  29208  fmcncfil  29801  sgn3da  30426  bnj605  30738  bnj594  30743  bnj1174  30832  bj-ssbequ2  32338  itg2gt0cn  33136  unirep  33178  ispridl2  33508  cnf1dd  33563  unisnALT  38684  ax6e2ndALT  38688  ssinc  38786  ssdec  38787  fmul01  39248  dvnmptconst  39493  dvnmul  39495  iccpartnel  40702  stgoldbwt  40989  sgoldbalt  40994  bgoldbtbnd  41016
  Copyright terms: Public domain W3C validator