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  1204  syl21anbrc  1209  syl21anc  1273  f1oiso2  5978  exmidapne  7539  nnnq0lem1  7726  prmuloc  7846  suplocexprlemex  8002  prsrlem1  8022  apreap  8826  lemulge11  9105  elnnz  9550  supinfneg  9890  infsupneg  9891  leexp1a  10919  faclbnd6  11069  zfz1isolem1  11167  oddpwdclemdc  12825  ennnfonelemf1  13119  grpidinv2  13721  rhmopp  14271  dvdsrzring  14699  cncnp2m  15042  upgrex  16044  uhgr2edg  16147  bj-charfun  16523