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  1684  axia3  2422  r19.26  2984  r19.29  2992  difrab  3779  dmcosseq  5274  fvn0fvelrn  6089  soxp  6912  smoord  7054  xpwdomg  8029  alephexp2  8973  lediv2a  10459  ssfzo12  11908  r19.29uz  13195  gsummoncoe1  18473  fbun  20467  wlkdvspthlem  24736  usgra2adedgspthlem2  24739  usgrcyclnl2  24768  erclwwlkeqlen  24939  eupatrl  25095  isdrngo3  30567  pm5.31r  30799  pm11.71  31507  fzoopth  32604  tratrb  33450  onfrALTlem3  33459  elex22VD  33782  en3lplem1VD  33786  tratrbVD  33804  undif3VD  33825  onfrALTlem3VD  33830  19.41rgVD  33845  2pm13.193VD  33846  ax6e2eqVD  33850  2uasbanhVD  33854  vk15.4jVD  33857
  Copyright terms: Public domain W3C validator