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  2110  imadiflem  5354  domssr  6871  supelti  7106  ltexnqq  7523  enq0sym  7547  enq0tr  7549  addclpr  7652  mulclpr  7687  ltexprlemopl  7716  ltexprlemlol  7717  ltexprlemopu  7718  ltexprlemupu  7719  suplocexprlemloc  7836  lemul12a  8937  elfzd  10140  fzass4  10186  elfz1b  10214  4fvwrd4  10264  leexp1a  10741  sqrt0rlem  11347  reumodprminv  12609  islmodd  14088  uptx  14779  distspace  14840  xmetxpbl  15013  bj-charfundc  15781