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  1177  syl21anbrc  1182  syl21anc  1237  f1oiso2  5828  exmidapne  7259  nnnq0lem1  7445  prmuloc  7565  suplocexprlemex  7721  prsrlem1  7741  apreap  8544  lemulge11  8823  elnnz  9263  supinfneg  9595  infsupneg  9596  leexp1a  10575  faclbnd6  10724  zfz1isolem1  10820  oddpwdclemdc  12173  ennnfonelemf1  12419  grpidinv2  12928  dvdsrzring  13496  cncnp2m  13734  bj-charfun  14562