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  1201  syl21anbrc  1206  syl21anc  1270  f1oiso2  5957  exmidapne  7457  nnnq0lem1  7644  prmuloc  7764  suplocexprlemex  7920  prsrlem1  7940  apreap  8745  lemulge11  9024  elnnz  9467  supinfneg  9802  infsupneg  9803  leexp1a  10828  faclbnd6  10978  zfz1isolem1  11075  oddpwdclemdc  12711  ennnfonelemf1  13005  grpidinv2  13607  rhmopp  14156  dvdsrzring  14583  cncnp2m  14921  upgrex  15919  uhgr2edg  16020  bj-charfun  16253