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  1132  19.29  1601  r19.26  2760  r19.29  2768  difrab  3530  dmcosseq  5049  soxp  6356  smoord  6524  xpwdomg  7446  alephexp2  8350  lediv2a  9797  r19.29uz  12041  fbun  17748  iundifdifd  23410  isdrngo3  26096  pm5.31r  26223  pm11.71  27102  wlkdvspthlem  27745  eupatrl  27765  usgrcyclnl2  27767  tratrb  28046  onfrALTlem3  28056  elex22VD  28379  en3lplem1VD  28383  tratrbVD  28401  undif3VD  28422  onfrALTlem3VD  28427  19.41rgVD  28442  2pm13.193VD  28443  a9e2eqVD  28447  2uasbanhVD  28451  vk15.4jVD  28454
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