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  1247  euan  2098  imadiflem  5333  supelti  7061  ltexnqq  7468  enq0sym  7492  enq0tr  7494  addclpr  7597  mulclpr  7632  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  suplocexprlemloc  7781  lemul12a  8881  elfzd  10082  fzass4  10128  elfz1b  10156  4fvwrd4  10206  leexp1a  10665  sqrt0rlem  11147  reumodprminv  12391  islmodd  13789  uptx  14442  distspace  14503  xmetxpbl  14676  bj-charfundc  15300