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  5896  exmidapne  7372  nnnq0lem1  7559  prmuloc  7679  suplocexprlemex  7835  prsrlem1  7855  apreap  8660  lemulge11  8939  elnnz  9382  supinfneg  9716  infsupneg  9717  leexp1a  10739  faclbnd6  10889  zfz1isolem1  10985  oddpwdclemdc  12495  ennnfonelemf1  12789  grpidinv2  13390  rhmopp  13938  dvdsrzring  14365  cncnp2m  14703  bj-charfun  15747