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  1248  euan  2112  imadiflem  5372  domssr  6892  supelti  7130  ltexnqq  7556  enq0sym  7580  enq0tr  7582  addclpr  7685  mulclpr  7720  ltexprlemopl  7749  ltexprlemlol  7750  ltexprlemopu  7751  ltexprlemupu  7752  suplocexprlemloc  7869  lemul12a  8970  elfzd  10173  fzass4  10219  elfz1b  10247  4fvwrd4  10297  leexp1a  10776  wrd2ind  11214  sqrt0rlem  11429  reumodprminv  12691  islmodd  14170  uptx  14861  distspace  14922  xmetxpbl  15095  bj-charfundc  15943