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  1585  r19.26  2677  r19.29  2685  difrab  3444  dmcosseq  4948  soxp  6230  smoord  6384  xpwdomg  7301  alephexp2  8205  lediv2a  9652  r19.29uz  11836  fbun  17537  iundifdifd  23161  and4as  24950  nxtand  24997  boxand  25017  prjmapcp2  25181  isdrngo3  26601  pm5.31r  26728  pm11.71  27607  tratrb  28355  onfrALTlem3  28365  elex22VD  28688  en3lplem1VD  28692  tratrbVD  28710  undif3VD  28731  onfrALTlem3VD  28736  19.41rgVD  28751  2pm13.193VD  28752  a9e2eqVD  28756  2uasbanhVD  28760  vk15.4jVD  28763
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