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  2646  r19.29  2654  difrab  3384  dmcosseq  4899  soxp  6127  smoord  6315  xpwdomg  7232  alephexp2  8136  lediv2a  9583  r19.29uz  11764  fbun  17462  and4as  24270  nxtand  24317  boxand  24337  prjmapcp2  24502  isdrngo3  25922  pm5.31r  26049  pm11.71  26928  tratrb  27315  onfrALTlem3  27325  elex22VD  27628  en3lplem1VD  27632  tratrbVD  27650  undif3VD  27671  onfrALTlem3VD  27676  19.41rgVD  27691  2pm13.193VD  27692  a9e2eqVD  27696  2uasbanhVD  27700  vk15.4jVD  27703
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