Theorem jca31 309

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 306	. 2 |- ( ph -> ( ps /\ ch ) )
4		jca31.3	. 2 |- ( ph -> th )
5	3, 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:  3jca  1203  syl21anbrc  1208  syl21anc  1272  f1oiso2  5968  exmidapne  7479  nnnq0lem1  7666  prmuloc  7786  suplocexprlemex  7942  prsrlem1  7962  apreap  8767  lemulge11  9046  elnnz  9489  supinfneg  9829  infsupneg  9830  leexp1a  10857  faclbnd6  11007  zfz1isolem1  11105  oddpwdclemdc  12763  ennnfonelemf1  13057  grpidinv2  13659  rhmopp  14209  dvdsrzring  14636  cncnp2m  14974  upgrex  15973  uhgr2edg  16076  bj-charfun  16453