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  5898  exmidapne  7374  nnnq0lem1  7561  prmuloc  7681  suplocexprlemex  7837  prsrlem1  7857  apreap  8662  lemulge11  8941  elnnz  9384  supinfneg  9718  infsupneg  9719  leexp1a  10741  faclbnd6  10891  zfz1isolem1  10987  oddpwdclemdc  12528  ennnfonelemf1  12822  grpidinv2  13423  rhmopp  13971  dvdsrzring  14398  cncnp2m  14736  bj-charfun  15780