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  1231  euan  2075  imadiflem  5275  supelti  6975  ltexnqq  7357  enq0sym  7381  enq0tr  7383  addclpr  7486  mulclpr  7521  ltexprlemopl  7550  ltexprlemlol  7551  ltexprlemopu  7552  ltexprlemupu  7553  suplocexprlemloc  7670  lemul12a  8765  fzass4  10005  elfz1b  10033  4fvwrd4  10083  leexp1a  10518  sqrt0rlem  10954  reumodprminv  12194  uptx  13027  distspace  13088  xmetxpbl  13261  bj-charfundc  13803