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  1217  euanOLD  2339  sbthlem9  7532  nqerf  9203  lemul12a  10291  lediv12a  10329  fzass4  11606  elfz1b  11637  4fvwrd4  11643  leexp1a  12032  wrd2ind  12483  cshwidxm1  12554  mreexexlem2d  14694  pmtrrn2  16077  islmodd  17069  rge0srg  18000  mdet1  18532  istps2OLD  18651  neitr  18909  restnlly  19211  llyrest  19214  llyidm  19217  uptx  19323  alexsubALTlem2  19745  alexsubALTlem4  19747  ivthlem3  21062  axtg5seg  23052  colperplem3  23252  f1otrg  23262  ax5seg  23329  axcontlem4  23358  eengtrkg  23376  grpoidinv  23840  pjnmopi  25697  cdj1i  25982  xrofsup  26199  dya2iocnrect  26833  sitgfval  26864  erdszelem7  27222  rellyscon  27277  relexpadd  27477  rtrclreclem.min  27486  segconeq  28178  ifscgr  28212  btwnconn1lem13  28267  btwnconn1lem14  28268  outsideofeq  28298  ellines  28320  itg2gt0cn  28588  frinfm  28770  heiborlem3  28853  isfldidl  29009  mzpincl  29211  mzpindd  29223  diophin  29252  pellexlem3  29313  pellexlem5  29315  stoweidlem1  29937  stoweidlem3  29939  stoweidlem14  29950  stoweidlem17  29953  stoweidlem27  29963  stoweidlem57  29993  reuan  30145  elfzelfzlble  30350  wwlkextinj  30503  wwlkextsur  30504  clwwlkf1  30599  usg2spot2nb  30799  lmod1  31144  cpmatmcllem  31184  bnj969  32242  bnj1463  32349  4atlem12  33565  cdleme48fv  34452  cdlemg35  34666  mapd0  35619