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  5827  exmidapne  7258  nnnq0lem1  7444  prmuloc  7564  suplocexprlemex  7720  prsrlem1  7740  apreap  8543  lemulge11  8822  elnnz  9262  supinfneg  9594  infsupneg  9595  leexp1a  10574  faclbnd6  10723  zfz1isolem1  10819  oddpwdclemdc  12172  ennnfonelemf1  12418  grpidinv2  12927  dvdsrzring  13463  cncnp2m  13701  bj-charfun  14529