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 804
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 393 1 ((𝜑 ∧ (𝜑𝜓)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  ornld  1048  r19.29vva  3229  2reu5  3568  intab  4641  dfac5  9151  grothpw  9850  grothpwex  9851  gcdcllem1  15429  gsmsymgreqlem2  18058  neindisj2  21148  tx1stc  21674  ufinffr  21953  ucnima  22305  frgr2wwlk1  27511  r19.29ffa  29660  fmcncfil  30317  sgn3da  30943  bnj605  31315  bnj594  31320  bnj1174  31409  bj-ssbequ2  32980  itg2gt0cn  33797  unirep  33839  ispridl2  34169  cnf1dd  34224  unisnALT  39684  ax6e2ndALT  39688  ssinc  39785  ssdec  39786  fmul01  40330  dvnmptconst  40674  dvnmul  40676  iccpartnel  41902  stgoldbwt  42192  sbgoldbalt  42197  bgoldbtbnd  42225
  Copyright terms: Public domain W3C validator