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  2798  r19.29  2806  difrab  3575  dmcosseq  5096  soxp  6418  smoord  6586  xpwdomg  7509  alephexp2  8412  lediv2a  9860  r19.29uz  12109  fbun  17825  wlkdvspthlem  21560  usgrcyclnl2  21581  eupatrl  21643  isdrngo3  26465  pm5.31r  26590  pm11.71  27464  ssfzo12  27990  usgra2adedgspthlem2  28044  tratrb  28331  onfrALTlem3  28341  elex22VD  28660  en3lplem1VD  28664  tratrbVD  28682  undif3VD  28703  onfrALTlem3VD  28708  19.41rgVD  28723  2pm13.193VD  28724  a9e2eqVD  28728  2uasbanhVD  28732  vk15.4jVD  28735
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