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 803
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 406 1 ((𝜑 ∧ (𝜑𝜓)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  ornld  1062  2reu5  3764  intab  4978  dfac5  10169  grothpw  10866  grothpwex  10867  gcdcllem1  16536  gsmsymgreqlem2  19449  neindisj2  23131  tx1stc  23658  ufinffr  23937  ucnima  24290  frgr2wwlk1  30348  r19.29ffa  32490  prmidl2  33469  fmcncfil  33930  sgn3da  34544  bnj605  34921  bnj594  34926  bnj1174  35017  itg2gt0cn  37682  unirep  37721  ispridl2  38045  cnf1dd  38097  faosnf0.11b  43440  dfsucon  43536  unisnALT  44946  ax6e2ndALT  44950  ssinc  45092  ssdec  45093  fmul01  45595  dvnmptconst  45956  dvnmul  45958  2reu8i  47125  iccpartnel  47425  stgoldbwt  47763  sbgoldbalt  47768  bgoldbtbnd  47796
  Copyright terms: Public domain W3C validator