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 187  df-an 371

This theorem is referenced by:  syl12anc  1230  sbthlem9  7675  nqerf  9340  lemul12a  10443  lediv12a  10480  fzass4  11778  elfz1b  11805  4fvwrd4  11850  leexp1a  12271  wrd2ind  12761  cshwidxm1  12835  rtrclreclem4  13045  mreexexlem2d  15261  sgrp2nmndlem4  16372  pmtrrn2  16811  islmodd  17840  nn0srg  18808  rge0srg  18809  mdet1  19397  cpmatmcllem  19513  istps2OLD  19716  neitr  19976  restnlly  20277  llyrest  20280  llyidm  20283  uptx  20420  alexsubALTlem2  20842  alexsubALTlem4  20844  ivthlem3  22159  axtg5seg  24243  colperpexlem3  24496  iscgra1  24571  f1otrg  24603  ax5seg  24670  axcontlem4  24699  eengtrkg  24717  wwlkextinj  25159  wwlkextsur  25160  clwwlkf1  25225  usg2spot2nb  25494  grpoidinv  25637  pjnmopi  27493  cdj1i  27778  xrofsup  28043  dya2iocnrect  28742  omssubadd  28761  sitgfval  28802  bnj969  29344  bnj1463  29451  erdszelem7  29507  rellyscon  29561  segconeq  30361  ifscgr  30395  btwnconn1lem13  30450  btwnconn1lem14  30451  outsideofeq  30481  ellines  30503  fnessref  30598  refssfne  30599  isbasisrelowllem1  31285  isbasisrelowllem2  31286  relowlssretop  31293  itg2gt0cn  31456  frinfm  31521  heiborlem3  31604  isfldidl  31760  4atlem12  32642  cdleme48fv  33531  cdlemg35  33745  mapd0  34698  mzpincl  35041  mzpindd  35053  diophin  35080  pellexlem3  35141  pellexlem5  35143  monoords  36878  mccllem  36986  sumnnodd  37017  lptre2pt  37027  dvnmul  37121  dvnprodlem1  37124  dvnprodlem2  37125  itgspltprt  37159  stoweidlem1  37164  stoweidlem3  37166  stoweidlem14  37177  stoweidlem17  37180  stoweidlem27  37190  stoweidlem57  37220  fourierdlem12  37282  fourierdlem14  37284  fourierdlem41  37311  fourierdlem48  37318  fourierdlem49  37319  fourierdlem50  37320  fourierdlem70  37340  fourierdlem79  37349  fourierdlem92  37362  fourierdlem111  37381  elaa2lem  37397  etransclem3  37401  etransclem7  37405  etransclem10  37408  etransclem24  37422  etransclem27  37425  etransclem28  37426  etransclem35  37433  etransclem38  37436  etransclem44  37442  reuan  37566  elfzelfzlble  37982  rngcinv  38313  rngcinvALTV  38325  ringcinv  38364  lmod1  38617