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  1269  euan  2134  imadiflem  5400  domssr  6937  supelti  7180  ltexnqq  7606  enq0sym  7630  enq0tr  7632  addclpr  7735  mulclpr  7770  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  suplocexprlemloc  7919  lemul12a  9020  elfzd  10224  fzass4  10270  elfz1b  10298  4fvwrd4  10348  leexp1a  10828  wrd2ind  11271  sqrt0rlem  11530  reumodprminv  12792  islmodd  14273  uptx  14964  distspace  15025  xmetxpbl  15198  bj-charfundc  16254