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  1586  r19.26  2688  r19.29  2696  difrab  3455  dmcosseq  4962  soxp  6244  smoord  6398  xpwdomg  7315  alephexp2  8219  lediv2a  9666  r19.29uz  11850  fbun  17551  iundifdifd  23175  and4as  25042  nxtand  25089  boxand  25109  prjmapcp2  25273  isdrngo3  26693  pm5.31r  26820  pm11.71  27699  wlkdvspthlem  28365  eupatrl  28385  usgrcyclnl2  28387  tratrb  28598  onfrALTlem3  28608  elex22VD  28931  en3lplem1VD  28935  tratrbVD  28953  undif3VD  28974  onfrALTlem3VD  28979  19.41rgVD  28994  2pm13.193VD  28995  a9e2eqVD  28999  2uasbanhVD  29003  vk15.4jVD  29006
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