Theorem jca32 537

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  syl12anc  1262  sbthlem9  7699  nqerf  9362  lemul12a  10470  lediv12a  10506  fzass4  11843  elfz1b  11871  4fvwrd4  11916  leexp1a  12337  wrd2ind  12836  cshwidxm1  12910  rtrclreclem4  13124  coprmproddvdslem  14678  prmgaplem6  15025  mreexexlem2d  15550  sgrp2nmndlem4  16661  pmtrrn2  17100  islmodd  18096  nn0srg  19035  rge0srg  19036  mdet1  19624  cpmatmcllem  19740  neitr  20194  restnlly  20495  llyrest  20498  llyidm  20501  uptx  20638  alexsubALTlem2  21061  alexsubALTlem4  21063  ivthlem3  22402  axtg5seg  24511  colperpexlem3  24772  outpasch  24795  iscgra1  24850  f1otrg  24899  ax5seg  24966  axcontlem4  24995  eengtrkg  25013  wwlkextinj  25456  wwlkextsur  25457  clwwlkf1  25522  usg2spot2nb  25791  grpoidinv  25934  pjnmopi  27799  cdj1i  28084  xrofsup  28359  dya2iocnrect  29111  omssubadd  29136  omssubaddOLD  29140  sitgfval  29182  bnj969  29765  bnj1463  29872  erdszelem7  29928  rellyscon  29982  segconeq  30782  ifscgr  30816  btwnconn1lem13  30871  btwnconn1lem14  30872  outsideofeq  30902  ellines  30924  fnessref  31018  refssfne  31019  isbasisrelowllem1  31722  isbasisrelowllem2  31723  relowlssretop  31730  itg2gt0cn  31961  frinfm  32026  heiborlem3  32109  isfldidl  32265  4atlem12  33146  cdleme48fv  34035  cdlemg35  34249  mapd0  35202  mzpincl  35545  mzpindd  35557  diophin  35584  pellexlem3  35645  pellexlem5  35647  amgm3d  36621  amgm4d  36622  monoords  37468  uzfissfz  37503  iuneqfzuzlem  37511  ssuzfz  37526  mccllem  37617  sumnnodd  37650  lptre2pt  37660  dvnmul  37758  dvnprodlem1  37761  dvnprodlem2  37762  itgspltprt  37796  stoweidlem1  37801  stoweidlem3  37803  stoweidlem14  37814  stoweidlem17  37817  stoweidlem27  37827  stoweidlem57  37858  fourierdlem12  37921  fourierdlem14  37923  fourierdlem41  37951  fourierdlem48  37958  fourierdlem49  37959  fourierdlem50  37960  fourierdlem70  37980  fourierdlem79  37989  fourierdlem92  38002  fourierdlem111  38021  elaa2lem  38037  elaa2lemOLD  38038  etransclem3  38042  etransclem7  38046  etransclem10  38049  etransclem24  38063  etransclem27  38066  etransclem28  38067  etransclem35  38074  etransclem38  38077  etransclem44  38083  iundjiun  38206  caratheodorylem1  38255  reuan  38472  elfzelfzlble  38915  rngcinv  39603  rngcinvALTV  39615  ringcinv  39654  lmod1  39907