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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  syl12anc  1276  euan  2143  imadiflem  5460  domssr  7064  supelti  7343  ltexnqq  7776  enq0sym  7800  enq0tr  7802  addclpr  7905  mulclpr  7940  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  suplocexprlemloc  8089  lemul12a  9195  elfzd  10430  fzass4  10479  elfz1b  10508  4fvwrd4  10558  infssfzcldc  10680  infssfzledc  10681  leexp1a  11046  wrd2ind  11511  sqrt0rlem  11785  reumodprminv  13055  islmodd  14713  uptx  15466  distspace  15527  xmetxpbl  15700  pellexlem3  16192  bj-charfundc  17000