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  1272  euan  2139  imadiflem  5437  domssr  7019  supelti  7295  ltexnqq  7725  enq0sym  7749  enq0tr  7751  addclpr  7854  mulclpr  7889  ltexprlemopl  7918  ltexprlemlol  7919  ltexprlemopu  7920  ltexprlemupu  7921  suplocexprlemloc  8038  lemul12a  9138  elfzd  10353  fzass4  10399  elfz1b  10428  4fvwrd4  10478  leexp1a  10960  wrd2ind  11419  sqrt0rlem  11692  reumodprminv  12955  islmodd  14458  uptx  15156  distspace  15217  xmetxpbl  15390  pellexlem3  15864  bj-charfundc  16595