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  2094  imadiflem  5314  supelti  7030  ltexnqq  7436  enq0sym  7460  enq0tr  7462  addclpr  7565  mulclpr  7600  ltexprlemopl  7629  ltexprlemlol  7630  ltexprlemopu  7631  ltexprlemupu  7632  suplocexprlemloc  7749  lemul12a  8848  elfzd  10045  fzass4  10091  elfz1b  10119  4fvwrd4  10169  leexp1a  10605  sqrt0rlem  11043  reumodprminv  12284  islmodd  13606  uptx  14226  distspace  14287  xmetxpbl  14460  bj-charfundc  15013