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  1167  19.29  1650  axia3  2410  r19.26  2849  r19.29  2857  difrab  3624  dmcosseq  5101  soxp  6685  smoord  6826  xpwdomg  7800  alephexp2  8745  lediv2a  10226  ssfzo12  11620  r19.29uz  12838  fbun  19413  wlkdvspthlem  23506  usgrcyclnl2  23527  eupatrl  23589  isdrngo3  28765  pm5.31r  28998  pm11.71  29650  fvn0fvelrn  30153  fzoopth  30213  usgra2adedgspthlem2  30304  erclwwlkeqlen  30482  gsummoncoe1  30843  tratrb  31242  onfrALTlem3  31252  elex22VD  31575  en3lplem1VD  31579  tratrbVD  31597  undif3VD  31618  onfrALTlem3VD  31623  19.41rgVD  31638  2pm13.193VD  31639  ax6e2eqVD  31643  2uasbanhVD  31647  vk15.4jVD  31650
  Copyright terms: Public domain W3C validator