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  5951  exmidapne  7446  nnnq0lem1  7633  prmuloc  7753  suplocexprlemex  7909  prsrlem1  7929  apreap  8734  lemulge11  9013  elnnz  9456  supinfneg  9790  infsupneg  9791  leexp1a  10816  faclbnd6  10966  zfz1isolem1  11062  oddpwdclemdc  12695  ennnfonelemf1  12989  grpidinv2  13591  rhmopp  14140  dvdsrzring  14567  cncnp2m  14905  upgrex  15903  uhgr2edg  16004  bj-charfun  16170