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

Theorem pm3.2 447
Description: Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Jan-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 22 . 2  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
21ex 434 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  pm3.21  448  pm3.2i  455  pm3.43i  456  ibar  504  jca  532  jcad  533  ancl  546  pm3.2an3  1175  19.29  1660  axia3  2432  r19.26  2989  r19.29  2997  difrab  3772  dmcosseq  5262  fvn0fvelrn  6076  soxp  6893  smoord  7033  xpwdomg  8007  alephexp2  8952  lediv2a  10435  ssfzo12  11869  r19.29uz  13139  gsummoncoe1  18114  fbun  20073  wlkdvspthlem  24282  usgra2adedgspthlem2  24285  usgrcyclnl2  24314  erclwwlkeqlen  24485  eupatrl  24641  isdrngo3  29963  pm5.31r  30196  pm11.71  30881  fzoopth  31809  tratrb  32386  onfrALTlem3  32396  elex22VD  32719  en3lplem1VD  32723  tratrbVD  32741  undif3VD  32762  onfrALTlem3VD  32767  19.41rgVD  32782  2pm13.193VD  32783  ax6e2eqVD  32787  2uasbanhVD  32791  vk15.4jVD  32794
  Copyright terms: Public domain W3C validator