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  1226  euanOLD  2354  sbthlem9  7632  nqerf  9304  lemul12a  10396  lediv12a  10434  fzass4  11717  elfz1b  11744  4fvwrd4  11786  leexp1a  12188  wrd2ind  12662  cshwidxm1  12736  mreexexlem2d  14896  pmtrrn2  16281  islmodd  17301  rge0srg  18255  mdet1  18870  cpmatmcllem  18986  istps2OLD  19189  neitr  19447  restnlly  19749  llyrest  19752  llyidm  19755  uptx  19861  alexsubALTlem2  20283  alexsubALTlem4  20285  ivthlem3  21600  axtg5seg  23590  colperpexlem3  23811  f1otrg  23850  ax5seg  23917  axcontlem4  23946  eengtrkg  23964  wwlkextinj  24406  wwlkextsur  24407  clwwlkf1  24472  usg2spot2nb  24742  grpoidinv  24886  pjnmopi  26743  cdj1i  27028  xrofsup  27250  dya2iocnrect  27892  sitgfval  27923  erdszelem7  28281  rellyscon  28336  relexpadd  28536  rtrclreclem.min  28545  segconeq  29237  ifscgr  29271  btwnconn1lem13  29326  btwnconn1lem14  29327  outsideofeq  29357  ellines  29379  itg2gt0cn  29647  frinfm  29829  heiborlem3  29912  isfldidl  30068  mzpincl  30270  mzpindd  30282  diophin  30310  pellexlem3  30371  pellexlem5  30373  monoords  31073  islptre  31161  sumnnodd  31172  iblspltprt  31291  itgspltprt  31297  stoweidlem1  31301  stoweidlem3  31303  stoweidlem14  31314  stoweidlem17  31317  stoweidlem27  31327  stoweidlem57  31357  fourierdlem12  31419  fourierdlem14  31421  fourierdlem41  31448  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem70  31477  fourierdlem79  31486  fourierdlem92  31499  reuan  31652  elfzelfzlble  31806  lmod1  32174  bnj969  33083  bnj1463  33190  4atlem12  34408  cdleme48fv  35295  cdlemg35  35509  mapd0  36462