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

Theorem pm3.35 573
Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)
Assertion
Ref Expression
pm3.35  |-  ( (
ph  /\  ( ph  ->  ps ) )  ->  ps )

Proof of Theorem pm3.35
StepHypRef Expression
1 pm2.27 37 . 2  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
21imp 420 1  |-  ( (
ph  /\  ( ph  ->  ps ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360
This theorem is referenced by:  intab  3790  dfac5  7639  grothpw  8328  grothpwex  8329  gcdcllem1  12564  neindisj2  16692  2ndcdisj  17014  tx1stc  17176  ufinffr  17456  cmptdst  24734  unirep  25515  ispridl2  25829  unisnALT  27392  notnot2ALT2  27393  a9e2ndALT  27397  bnj605  27628  bnj594  27633  bnj1174  27722
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator