Theorem jca32 535

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 532	. 2 |- ( ph -> ( ch /\ th ) )
5	1, 4	jca 532	1 |- ( ph -> ( ps /\ ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 369

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

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  syl12anc  1216  euanOLD  2330  sbthlem9  7421  nqerf  9091  lemul12a  10179  lediv12a  10217  fzass4  11488  elfz1b  11519  4fvwrd4  11525  leexp1a  11914  wrd2ind  12364  cshwidxm1  12435  mreexexlem2d  14575  pmtrrn2  15957  islmodd  16932  rge0srg  17857  istps2OLD  18501  neitr  18759  restnlly  19061  llyrest  19064  llyidm  19067  uptx  19173  alexsubALTlem2  19595  alexsubALTlem4  19597  ivthlem3  20912  axtg5seg  22901  f1otrg  23068  ax5seg  23135  axcontlem4  23164  eengtrkg  23182  grpoidinv  23646  pjnmopi  25503  cdj1i  25788  xrofsup  26006  dya2iocnrect  26648  sitgfval  26679  erdszelem7  27037  rellyscon  27092  relexpadd  27291  rtrclreclem.min  27300  segconeq  27992  ifscgr  28026  btwnconn1lem13  28081  btwnconn1lem14  28082  outsideofeq  28112  ellines  28134  itg2gt0cn  28400  frinfm  28582  heiborlem3  28665  isfldidl  28821  mzpincl  29023  mzpindd  29035  diophin  29064  pellexlem3  29125  pellexlem5  29127  stoweidlem1  29749  stoweidlem3  29751  stoweidlem14  29762  stoweidlem17  29765  stoweidlem27  29775  stoweidlem57  29805  reuan  29957  elfzelfzlble  30162  wwlkextinj  30315  wwlkextsur  30316  clwwlkf1  30411  usg2spot2nb  30611  lmod1  30923  bnj969  31826  bnj1463  31933  4atlem12  33096  cdleme48fv  33983  cdlemg35  34197  mapd0  35150