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  1272  euan  2136  imadiflem  5416  domssr  6994  supelti  7261  ltexnqq  7688  enq0sym  7712  enq0tr  7714  addclpr  7817  mulclpr  7852  ltexprlemopl  7881  ltexprlemlol  7882  ltexprlemopu  7883  ltexprlemupu  7884  suplocexprlemloc  8001  lemul12a  9101  elfzd  10313  fzass4  10359  elfz1b  10387  4fvwrd4  10437  leexp1a  10919  wrd2ind  11370  sqrt0rlem  11643  reumodprminv  12906  islmodd  14389  uptx  15085  distspace  15146  xmetxpbl  15319  pellexlem3  15793  bj-charfundc  16524