Theorem jca31 305

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  3jca  1129  syl21anc  1183  f1oiso2  5660  nnnq0lem1  7155  prmuloc  7275  prsrlem1  7438  apreap  8215  lemulge11  8482  elnnz  8916  supinfneg  9240  infsupneg  9241  leexp1a  10189  faclbnd6  10331  zfz1isolem1  10424  oddpwdclemdc  11643  ennnfonelemf1  11723  cncnp2m  12181