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

Theorem pm3.2 436
Description: Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
Assertion
Ref Expression
pm3.2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )

Proof of Theorem pm3.2
StepHypRef Expression
1 id 21 . 2  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
21ex 425 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360
This theorem is referenced by:  pm3.21  437  pm3.2i  443  pm3.43i  444  ibar  492  jca  520  jcad  521  ancl  531  pm3.2an3  1136  19.29  1595  r19.26  2650  r19.29  2658  difrab  3417  dmcosseq  4934  soxp  6162  smoord  6350  xpwdomg  7267  alephexp2  8171  lediv2a  9618  r19.29uz  11800  fbun  17498  and4as  24306  nxtand  24353  boxand  24373  prjmapcp2  24538  isdrngo3  25958  pm5.31r  26085  pm11.71  26964  tratrb  27435  onfrALTlem3  27445  elex22VD  27748  en3lplem1VD  27752  tratrbVD  27770  undif3VD  27791  onfrALTlem3VD  27796  19.41rgVD  27811  2pm13.193VD  27812  a9e2eqVD  27816  2uasbanhVD  27820  vk15.4jVD  27823
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