MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.2 Unicode version

Theorem pm3.2 435
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 20 . 2  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
21ex 424 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  pm3.21  436  pm3.2i  442  pm3.43i  443  ibar  491  jca  519  jcad  520  ancl  530  pm3.2an3  1133  19.29  1603  r19.26  2782  r19.29  2790  difrab  3559  dmcosseq  5078  soxp  6396  smoord  6564  xpwdomg  7487  alephexp2  8390  lediv2a  9837  r19.29uz  12082  fbun  17794  wlkdvspthlem  21456  usgrcyclnl2  21477  eupatrl  21539  isdrngo3  26267  pm5.31r  26392  pm11.71  27266  tratrb  27964  onfrALTlem3  27974  elex22VD  28293  en3lplem1VD  28297  tratrbVD  28315  undif3VD  28336  onfrALTlem3VD  28341  19.41rgVD  28356  2pm13.193VD  28357  a9e2eqVD  28361  2uasbanhVD  28365  vk15.4jVD  28368
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 178  df-an 361
  Copyright terms: Public domain W3C validator