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  1180  syl21anbrc  1185  syl21anc  1249  f1oiso2  5919  exmidapne  7407  nnnq0lem1  7594  prmuloc  7714  suplocexprlemex  7870  prsrlem1  7890  apreap  8695  lemulge11  8974  elnnz  9417  supinfneg  9751  infsupneg  9752  leexp1a  10776  faclbnd6  10926  zfz1isolem1  11022  oddpwdclemdc  12610  ennnfonelemf1  12904  grpidinv2  13505  rhmopp  14053  dvdsrzring  14480  cncnp2m  14818  upgrex  15814  bj-charfun  15942