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  2676  r19.29  2684  difrab  3443  dmcosseq  4945  soxp  6190  smoord  6378  xpwdomg  7295  alephexp2  8199  lediv2a  9646  r19.29uz  11830  fbun  17531  and4as  24349  nxtand  24396  boxand  24416  prjmapcp2  24581  isdrngo3  26001  pm5.31r  26128  pm11.71  27007  tratrb  27582  onfrALTlem3  27592  elex22VD  27895  en3lplem1VD  27899  tratrbVD  27917  undif3VD  27938  onfrALTlem3VD  27943  19.41rgVD  27958  2pm13.193VD  27959  a9e2eqVD  27963  2uasbanhVD  27967  vk15.4jVD  27970
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