Theorem jca32 308

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 304	. 2 |- ( ph -> ( ch /\ th ) )
5	1, 4	jca 304	1 |- ( ph -> ( ps /\ ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  syl12anc  1214  euan  2053  imadiflem  5197  supelti  6882  ltexnqq  7209  enq0sym  7233  enq0tr  7235  addclpr  7338  mulclpr  7373  ltexprlemopl  7402  ltexprlemlol  7403  ltexprlemopu  7404  ltexprlemupu  7405  suplocexprlemloc  7522  lemul12a  8613  fzass4  9835  elfz1b  9863  4fvwrd4  9910  leexp1a  10341  sqrt0rlem  10768  uptx  12432  distspace  12493  xmetxpbl  12666