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  2101  imadiflem  5338  supelti  7070  ltexnqq  7478  enq0sym  7502  enq0tr  7504  addclpr  7607  mulclpr  7642  ltexprlemopl  7671  ltexprlemlol  7672  ltexprlemopu  7673  ltexprlemupu  7674  suplocexprlemloc  7791  lemul12a  8892  elfzd  10094  fzass4  10140  elfz1b  10168  4fvwrd4  10218  leexp1a  10689  sqrt0rlem  11171  reumodprminv  12433  islmodd  13875  uptx  14536  distspace  14597  xmetxpbl  14770  bj-charfundc  15480