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  1269  euan  2134  imadiflem  5400  domssr  6929  supelti  7169  ltexnqq  7595  enq0sym  7619  enq0tr  7621  addclpr  7724  mulclpr  7759  ltexprlemopl  7788  ltexprlemlol  7789  ltexprlemopu  7790  ltexprlemupu  7791  suplocexprlemloc  7908  lemul12a  9009  elfzd  10212  fzass4  10258  elfz1b  10286  4fvwrd4  10336  leexp1a  10816  wrd2ind  11255  sqrt0rlem  11514  reumodprminv  12776  islmodd  14257  uptx  14948  distspace  15009  xmetxpbl  15182  bj-charfundc  16171