Theorem jca32 542

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  syl12anc  1274  sbthlem9  7721  nqerf  9386  lemul12a  10496  lediv12a  10532  fzass4  11871  elfz1b  11899  4fvwrd4  11946  leexp1a  12369  wrd2ind  12877  cshwidxm1  12951  rtrclreclem4  13179  coprmproddvdslem  14734  prmgaplem6  15081  mreexexlem2d  15606  sgrp2nmndlem4  16717  pmtrrn2  17156  islmodd  18152  nn0srg  19092  rge0srg  19093  mdet1  19681  cpmatmcllem  19797  neitr  20251  restnlly  20552  llyrest  20555  llyidm  20558  uptx  20695  alexsubALTlem2  21118  alexsubALTlem4  21120  ivthlem3  22459  axtg5seg  24569  colperpexlem3  24830  outpasch  24853  iscgra1  24908  f1otrg  24957  ax5seg  25024  axcontlem4  25053  eengtrkg  25071  wwlkextinj  25514  wwlkextsur  25515  clwwlkf1  25580  usg2spot2nb  25849  grpoidinv  25992  pjnmopi  27857  cdj1i  28142  xrofsup  28405  dya2iocnrect  29153  omssubadd  29178  omssubaddOLD  29182  sitgfval  29224  bnj969  29807  bnj1463  29914  erdszelem7  29970  rellyscon  30024  segconeq  30827  ifscgr  30861  btwnconn1lem13  30916  btwnconn1lem14  30917  outsideofeq  30947  ellines  30969  fnessref  31063  refssfne  31064  isbasisrelowllem1  31804  isbasisrelowllem2  31805  relowlssretop  31812  itg2gt0cn  32043  frinfm  32108  heiborlem3  32191  isfldidl  32347  4atlem12  33223  cdleme48fv  34112  cdlemg35  34326  mapd0  35279  mzpincl  35622  mzpindd  35634  diophin  35661  pellexlem3  35721  pellexlem5  35723  amgm3d  36696  amgm4d  36697  monoords  37589  uzfissfz  37624  iuneqfzuzlem  37632  ssuzfz  37647  mccllem  37763  sumnnodd  37796  lptre2pt  37806  dvnmul  37904  dvnprodlem1  37907  dvnprodlem2  37908  itgspltprt  37942  stoweidlem1  37962  stoweidlem3  37964  stoweidlem14  37975  stoweidlem17  37978  stoweidlem27  37988  stoweidlem57  38019  fourierdlem12  38082  fourierdlem14  38084  fourierdlem41  38112  fourierdlem48  38119  fourierdlem49  38120  fourierdlem50  38121  fourierdlem70  38141  fourierdlem79  38150  fourierdlem92  38163  fourierdlem111  38182  elaa2lem  38198  elaa2lemOLD  38199  etransclem3  38203  etransclem7  38207  etransclem10  38210  etransclem24  38224  etransclem27  38227  etransclem28  38228  etransclem35  38235  etransclem38  38238  etransclem44  38244  salgenval  38283  iundjiun  38403  caratheodorylem1  38455  reuan  38736  elfzelfzlble  39199  rngcinv  40352  rngcinvALTV  40364  ringcinv  40403  lmod1  40654