MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.35 Unicode version

Theorem pm3.35 587
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 39 . 2
21imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  r19.29af2  2969  r19.29_2a  2973  2reu5  3278  intab  4275  dfac5  8435  grothpw  9130  grothpwex  9131  gcdcllem1  13853  gsmsymgreqlem2  16095  neindisj2  19126  tx1stc  19622  ufinffr  19901  ucnima  20255  tgldim0eq  23358  fmcncfil  26818  sgn3da  27380  itg2gt0cn  28907  unirep  29066  ispridl2  29298  cnf1dd  29353  impel  29366  fmul01  30359  iblspltprt  30520  itgspltprt  30526  ccats1rev  31137  unisnALT  32505  ax6e2ndALT  32509  bnj605  32743  bnj594  32748  bnj1174  32837
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 185  df-an 371
  Copyright terms: Public domain W3C validator