Theorem jca32 310

Description: Join three consequents. (Contributed by FL, 1-Aug-2009.)

Hypotheses

Ref	Expression
jca31.1	|- ( ph -> ps )
jca31.2	|- ( ph -> ch )
jca31.3	|- ( ph -> th )

Assertion

Ref	Expression
jca32	|- ( ph -> ( ps /\ ( ch /\ th ) ) )

Proof of Theorem jca32

Step	Hyp	Ref	Expression
1		jca31.1	. 2 |- ( ph -> ps )
2		jca31.2	. . 3 |- ( ph -> ch )
3		jca31.3	. . 3 |- ( ph -> th )
4	2, 3	jca 306	. 2 |- ( ph -> ( ch /\ th ) )
5	1, 4	jca 306	1 |- ( ph -> ( ps /\ ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  syl12anc  1248  euan  2110  imadiflem  5353  domssr  6869  supelti  7104  ltexnqq  7521  enq0sym  7545  enq0tr  7547  addclpr  7650  mulclpr  7685  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  suplocexprlemloc  7834  lemul12a  8935  elfzd  10138  fzass4  10184  elfz1b  10212  4fvwrd4  10262  leexp1a  10739  sqrt0rlem  11314  reumodprminv  12576  islmodd  14055  uptx  14746  distspace  14807  xmetxpbl  14980  bj-charfundc  15748