MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.2 Structured version   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  1606  axia3  2403  r19.26  2830  r19.29  2838  difrab  3607  dmcosseq  5129  soxp  6451  smoord  6619  xpwdomg  7545  alephexp2  8448  lediv2a  9896  r19.29uz  12146  fbun  17864  wlkdvspthlem  21599  usgrcyclnl2  21620  eupatrl  21682  isdrngo3  26556  pm5.31r  26681  pm11.71  27554  ssfzo12  28103  usgra2adedgspthlem2  28257  tratrb  28547  onfrALTlem3  28557  elex22VD  28878  en3lplem1VD  28882  tratrbVD  28900  undif3VD  28921  onfrALTlem3VD  28926  19.41rgVD  28941  2pm13.193VD  28942  a9e2eqVD  28946  2uasbanhVD  28950  vk15.4jVD  28953
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