Theorem jca32 308

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 304	. 2 |- ( ph -> ( ch /\ th ) )
5	1, 4	jca 304	1 |- ( ph -> ( ps /\ ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  syl12anc  1226  euan  2070  imadiflem  5267  supelti  6967  ltexnqq  7349  enq0sym  7373  enq0tr  7375  addclpr  7478  mulclpr  7513  ltexprlemopl  7542  ltexprlemlol  7543  ltexprlemopu  7544  ltexprlemupu  7545  suplocexprlemloc  7662  lemul12a  8757  fzass4  9997  elfz1b  10025  4fvwrd4  10075  leexp1a  10510  sqrt0rlem  10945  reumodprminv  12185  uptx  12914  distspace  12975  xmetxpbl  13148  bj-charfundc  13690