Theorem jca32 306

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  syl12anc  1197  euan  2031  imadiflem  5160  supelti  6841  ltexnqq  7164  enq0sym  7188  enq0tr  7190  addclpr  7293  mulclpr  7328  ltexprlemopl  7357  ltexprlemlol  7358  ltexprlemopu  7359  ltexprlemupu  7360  lemul12a  8530  fzass4  9735  elfz1b  9763  4fvwrd4  9810  leexp1a  10241  sqrt0rlem  10667  uptx  12285  distspace  12324  xmetxpbl  12497