Theorem jca32 532

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 529	. 2 |- ( ph -> ( ch /\ th ) )
5	1, 4	jca 529	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  1209  euanOLD  2329  sbthlem9  7417  nqerf  9086  lemul12a  10174  lediv12a  10212  fzass4  11482  elfz1b  11510  4fvwrd4  11516  leexp1a  11905  wrd2ind  12355  cshwidxm1  12426  mreexexlem2d  14565  pmtrrn2  15945  islmodd  16877  istps2OLD  18367  neitr  18625  restnlly  18927  llyrest  18930  llyidm  18933  uptx  19039  alexsubALTlem2  19461  alexsubALTlem4  19463  ivthlem3  20778  axtg5seg  22810  f1otrg  22939  ax5seg  23006  axcontlem4  23035  eengtrkg  23053  grpoidinv  23517  pjnmopi  25374  cdj1i  25659  xrofsup  25877  rge0srg  26063  dya2iocnrect  26549  sitgfval  26574  erdszelem7  26932  rellyscon  26987  relexpadd  27186  rtrclreclem.min  27195  segconeq  27887  ifscgr  27921  btwnconn1lem13  27976  btwnconn1lem14  27977  outsideofeq  28007  ellines  28029  itg2gt0cn  28288  frinfm  28470  heiborlem3  28553  isfldidl  28709  mzpincl  28912  mzpindd  28924  diophin  28953  pellexlem3  29014  pellexlem5  29016  stoweidlem1  29639  stoweidlem3  29641  stoweidlem14  29652  stoweidlem17  29655  stoweidlem57  29695  reuan  29847  elfzelfzlble  30052  wwlkextinj  30205  wwlkextsur  30206  clwwlkf1  30301  usg2spot2nb  30501  lmod1  30740  bnj969  31638  bnj1463  31745  4atlem12  32826  cdleme48fv  33713  cdlemg35  33927  mapd0  34880