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  2637  r19.29  2645  difrab  3349  dmcosseq  4853  soxp  6080  smoord  6268  xpwdomg  7183  alephexp2  8083  lediv2a  9530  r19.29uz  11711  fbun  17367  and4as  24104  nxtand  24151  boxand  24171  prjmapcp2  24336  isdrngo3  25756  pm5.31r  25883  pm11.71  26762  tratrb  26992  onfrALTlem3  27002  elex22VD  27305  en3lplem1VD  27309  tratrbVD  27327  undif3VD  27348  onfrALTlem3VD  27353  19.41rgVD  27368  2pm13.193VD  27369  a9e2eqVD  27373  2uasbanhVD  27377  vk15.4jVD  27380
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