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

Theorem pm3.2 434
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 19 . 2  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
21ex 423 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  pm3.21  435  pm3.2i  441  pm3.43i  442  ibar  490  jca  518  jcad  519  ancl  529  pm3.2an3  1131  19.29  1583  r19.26  2675  r19.29  2683  difrab  3442  dmcosseq  4946  soxp  6228  smoord  6382  xpwdomg  7299  alephexp2  8203  lediv2a  9650  r19.29uz  11834  fbun  17535  iundifdifd  23159  and4as  24939  nxtand  24986  boxand  25006  prjmapcp2  25170  isdrngo3  26590  pm5.31r  26717  pm11.71  27596  tratrb  28299  onfrALTlem3  28309  elex22VD  28615  en3lplem1VD  28619  tratrbVD  28637  undif3VD  28658  onfrALTlem3VD  28663  19.41rgVD  28678  2pm13.193VD  28679  a9e2eqVD  28683  2uasbanhVD  28687  vk15.4jVD  28690
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator