Theorem pm3.2 463

Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. See pm3.2im 157 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

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ( ph /\ ps ) -> ( ph /\ ps ) )
2	1	ex 450	1 |- ( ph -> ( ps -> ( ph /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  pm3.21  464  pm3.2i  471  pm3.43i  472  ibar  525  jca  554  jcad  555  ancl  569  pm3.2an3OLD  1241  19.29  1801  19.40b  1815  19.42-1  2104  axia3  2589  r19.26  3064  r19.29  3072  difrab  3901  reuss2  3907  dmcosseq  5387  fvn0fvelrn  6430  soxp  7290  smoord  7462  xpwdomg  8490  alephexp2  9403  lediv2a  10917  ssfzo12  12561  r19.29uz  14090  gsummoncoe1  19674  fbun  21644  isdrngo3  33758  pm5.31r  34143  or3or  38319  pm11.71  38597  tratrb  38746  onfrALTlem3  38759  elex22VD  39074  en3lplem1VD  39078  tratrbVD  39097  undif3VD  39118  onfrALTlem3VD  39123  19.41rgVD  39138  2pm13.193VD  39139  ax6e2eqVD  39143  2uasbanhVD  39147  vk15.4jVD  39150  fzoopth  41337