Theorem jca32 558

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

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  syl12anc  1324  sbthlem9  8078  nqerf  9752  lemul12a  10881  lediv12a  10916  fzass4  12379  4fvwrd4  12459  leexp1a  12919  wrd2ind  13477  cshwidxm1  13553  rtrclreclem4  13801  coprmproddvdslem  15376  prmgaplem6  15760  mreexexlem2d  16305  sgrp2nmndlem4  17415  pmtrrn2  17880  islmodd  18869  nn0srg  19816  rge0srg  19817  mdet1  20407  cpmatmcllem  20523  neitr  20984  restnlly  21285  llyrest  21288  llyidm  21291  uptx  21428  alexsubALTlem2  21852  alexsubALTlem4  21854  distspace  22121  ncvs1  22957  ivthlem3  23222  axtg5seg  25364  colperpexlem3  25624  outpasch  25647  iscgra1  25702  f1otrg  25751  ax5seg  25818  axcontlem4  25847  eengtrkg  25865  wlkonwlk1l  26559  crctcshwlkn0  26713  wwlksnextinj  26794  wwlksnextsur  26795  clwwlksf1  26917  grpoidinv  27362  pjnmopi  29007  cdj1i  29292  xrofsup  29533  dya2iocnrect  30343  omssubadd  30362  sitgfval  30403  bnj969  31016  bnj1463  31123  erdszelem7  31179  rellysconn  31233  conway  31910  etasslt  31920  segconeq  32117  ifscgr  32151  btwnconn1lem13  32206  btwnconn1lem14  32207  outsideofeq  32237  ellines  32259  fnessref  32352  refssfne  32353  knoppndvlem14  32516  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlssretop  33211  itg2gt0cn  33465  frinfm  33530  heiborlem3  33612  isfldidl  33867  4atlem12  34898  cdleme48fv  35787  cdlemg35  36001  mapd0  36954  mzpincl  37297  mzpindd  37309  diophin  37336  pellexlem3  37395  pellexlem5  37397  amgm3d  38502  amgm4d  38503  monoords  39511  uzfissfz  39542  iuneqfzuzlem  39550  ssuzfz  39565  elfzd  39636  mccllem  39829  sumnnodd  39862  lptre2pt  39872  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  itgspltprt  40195  stoweidlem1  40218  stoweidlem3  40220  stoweidlem14  40231  stoweidlem17  40234  stoweidlem27  40244  stoweidlem57  40274  fourierdlem12  40336  fourierdlem14  40338  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem70  40393  fourierdlem79  40402  fourierdlem92  40415  fourierdlem111  40434  elaa2lem  40450  etransclem3  40454  etransclem7  40458  etransclem10  40461  etransclem24  40475  etransclem27  40478  etransclem28  40479  etransclem35  40486  etransclem38  40489  etransclem44  40495  salgenval  40541  iundjiun  40677  caratheodorylem1  40740  smfaddlem1  40971  reuan  41180  elfzelfzlble  41331  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  lmod1  42281