Theorem jca31 307

Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
jca31.1	|- ( ph -> ps )
jca31.2	|- ( ph -> ch )
jca31.3	|- ( ph -> th )

Assertion

Ref	Expression
jca31	|- ( ph -> ( ( ps /\ ch ) /\ th ) )

Proof of Theorem jca31

Step	Hyp	Ref	Expression
1		jca31.1	. . 3 |- ( ph -> ps )
2		jca31.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 304	. 2 |- ( ph -> ( ps /\ ch ) )
4		jca31.3	. 2 |- ( ph -> th )
5	3, 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:  3jca  1161  syl21anc  1215  f1oiso2  5728  nnnq0lem1  7254  prmuloc  7374  suplocexprlemex  7530  prsrlem1  7550  apreap  8349  lemulge11  8624  elnnz  9064  supinfneg  9390  infsupneg  9391  leexp1a  10348  faclbnd6  10490  zfz1isolem1  10583  oddpwdclemdc  11851  ennnfonelemf1  11931  cncnp2m  12400