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  1225  euan  2069  imadiflem  5261  supelti  6958  ltexnqq  7340  enq0sym  7364  enq0tr  7366  addclpr  7469  mulclpr  7504  ltexprlemopl  7533  ltexprlemlol  7534  ltexprlemopu  7535  ltexprlemupu  7536  suplocexprlemloc  7653  lemul12a  8748  fzass4  9987  elfz1b  10015  4fvwrd4  10065  leexp1a  10500  sqrt0rlem  10931  reumodprminv  12162  uptx  12815  distspace  12876  xmetxpbl  13049  bj-charfundc  13525