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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  3jca  1208  syl21anbrc  1213  syl21anc  1277  f1oiso2  6033  exmidapne  7626  nnnq0lem1  7813  prmuloc  7933  suplocexprlemex  8089  prsrlem1  8109  apreap  8917  lemulge11  9198  elnnz  9658  supinfneg  10004  infsupneg  10005  leexp1a  11044  faclbnd6  11196  zfz1isolem1  11306  nnmaxpwlemparts  12968  ennnfonelemf1  13358  grpidinv2  13912  rhmopp  14532  dvdsrzring  14987  cncnp2m  15381  upgrex  16442  uhgr2edg  16545  bj-charfun  16931