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

Theorem pm3.2 436
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 21 . 2  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
21ex 425 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  pm3.21  437  pm3.2i  443  pm3.43i  444  ibar  492  jca  520  jcad  521  ancl  531  pm3.2an3  1134  19.29  1607  axia3  2406  r19.26  2840  r19.29  2848  difrab  3617  dmcosseq  5140  soxp  6462  smoord  6630  xpwdomg  7556  alephexp2  8461  lediv2a  9909  r19.29uz  12159  fbun  17877  wlkdvspthlem  21612  usgrcyclnl2  21633  eupatrl  21695  isdrngo3  26588  pm5.31r  26713  pm11.71  27586  ssfzo12  28152  fzoopth  28161  usgra2adedgspthlem2  28351  tratrb  28693  onfrALTlem3  28703  elex22VD  29024  en3lplem1VD  29028  tratrbVD  29046  undif3VD  29067  onfrALTlem3VD  29072  19.41rgVD  29087  2pm13.193VD  29088  a9e2eqVD  29092  2uasbanhVD  29096  vk15.4jVD  29099
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 179  df-an 362
  Copyright terms: Public domain W3C validator