Theorem jca32 521

Description: Join three consequents. (Contributed by FL, 1-Aug-2009.)

Hypotheses

Ref	Expression
jca31.1	|- ( ph -> ps )
jca31.2	|- ( ph -> ch )
jca31.3	|- ( ph -> th )

Assertion

Ref	Expression
jca32	|- ( ph -> ( ps /\ ( ch /\ th ) ) )

Proof of Theorem jca32

Step	Hyp	Ref	Expression
1		jca31.1	. 2 |- ( ph -> ps )
2		jca31.2	. . 3 |- ( ph -> ch )
3		jca31.3	. . 3 |- ( ph -> th )
4	2, 3	jca 518	. 2 |- ( ph -> ( ch /\ th ) )
5	1, 4	jca 518	1 |- ( ph -> ( ps /\ ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 358

This theorem is referenced by:  syl12anc  1180  euan  2200  sbthlem9  6979  nqerf  8554  lemul12a  9614  lediv12a  9649  fzass4  10829  leexp1a  11160  mreexexlem2d  13547  islmodd  15633  istps2OLD  16659  restnlly  17208  llyrest  17211  llyidm  17214  uptx  17319  alexsubALTlem2  17742  alexsubALTlem4  17744  ivthlem3  18813  grpoidinv  20875  pjnmopi  22728  cdj1i  23013  probun  23622  erdszelem7  23728  rellyscon  23782  relexpadd  24035  rtrclreclem.min  24044  ax5seg  24566  axcontlem4  24595  segconeq  24633  ifscgr  24667  btwnconn1lem13  24722  btwnconn1lem14  24723  outsideofeq  24753  ellines  24775  repcpwti  25161  domncnt  25282  bisig0  26062  frinfm  26416  heiborlem3  26537  isfldidl  26693  mzpincl  26812  mzpindd  26824  diophin  26852  pellexlem3  26916  pellexlem5  26918  wallispilem1  27814  reuan  27958  bnj969  28978  bnj1463  29085  4atlem12  29801  cdleme48fv  30688  cdlemg35  30902  mapd0  31855

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177  df-an 360