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 612
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 444 1 ((𝜑 ∧ (𝜑𝜓)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  ornld  976  r19.29vva  3217  2reu5  3555  intab  4657  dfac5  9139  grothpw  9838  grothpwex  9839  gcdcllem1  15421  gsmsymgreqlem2  18049  neindisj2  21127  tx1stc  21653  ufinffr  21932  ucnima  22284  frgr2wwlk1  27481  r19.29ffa  29627  fmcncfil  30284  sgn3da  30910  bnj605  31282  bnj594  31287  bnj1174  31376  bj-ssbequ2  32947  itg2gt0cn  33776  unirep  33818  ispridl2  34148  cnf1dd  34203  unisnALT  39659  ax6e2ndALT  39663  ssinc  39761  ssdec  39762  fmul01  40313  dvnmptconst  40657  dvnmul  40659  iccpartnel  41882  stgoldbwt  42172  sbgoldbalt  42177  bgoldbtbnd  42205
  Copyright terms: Public domain W3C validator