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

Theorem pm3.2 449
Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. See pm3.2im 149 for a version using only implication and negation. (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 436 1  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  pm3.21  450  pm3.2i  457  pm3.43i  458  ibar  507  jca  535  jcad  536  ancl  549  pm3.2an3  1187  19.29  1735  19.40b  1750  axia3  2418  r19.26  2917  r19.29  2925  difrab  3717  dmcosseq  5096  fvn0fvelrn  6081  soxp  6909  smoord  7084  xpwdomg  8100  alephexp2  9006  lediv2a  10500  ssfzo12  12004  r19.29uz  13413  gsummoncoe1  18898  fbun  20855  wlkdvspthlem  25337  usgra2adedgspthlem2  25340  usgrcyclnl2  25369  erclwwlkeqlen  25540  eupatrl  25696  isdrngo3  32198  pm5.31r  32427  pm11.71  36747  tratrb  36897  onfrALTlem3  36910  elex22VD  37235  en3lplem1VD  37239  tratrbVD  37258  undif3VD  37279  onfrALTlem3VD  37284  19.41rgVD  37299  2pm13.193VD  37300  ax6e2eqVD  37304  2uasbanhVD  37308  vk15.4jVD  37311  fzoopth  39063  usgr2edg  39291
  Copyright terms: Public domain W3C validator