Theorem jca32 523

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

Syntax hints:   -> wi 4   /\ wa 360

This theorem is referenced by:  syl12anc  1183  euan  2344  sbthlem9  7254  nqerf  8838  lemul12a  9899  lediv12a  9934  fzass4  11121  4fvwrd4  11152  leexp1a  11469  mreexexlem2d  13901  islmodd  15987  istps2OLD  17017  neitr  17275  restnlly  17576  llyrest  17579  llyidm  17582  uptx  17688  alexsubALTlem2  18110  alexsubALTlem4  18112  ivthlem3  19381  grpoidinv  21827  pjnmopi  23682  cdj1i  23967  xrofsup  24157  dya2iocnrect  24662  sitgfval  24686  erdszelem7  24914  rellyscon  24969  relexpadd  25169  rtrclreclem.min  25178  ax5seg  25908  axcontlem4  25937  segconeq  25975  ifscgr  26009  btwnconn1lem13  26064  btwnconn1lem14  26065  outsideofeq  26095  ellines  26117  itg2gt0cn  26298  frinfm  26475  heiborlem3  26560  isfldidl  26716  mzpincl  26829  mzpindd  26841  diophin  26869  pellexlem3  26932  pellexlem5  26934  stoweidlem1  27764  stoweidlem3  27766  stoweidlem14  27777  stoweidlem17  27780  stoweidlem57  27820  reuan  27972  2cshw2lem1  28310  2cshw2lem2  28311  usg2spot2nb  28552  bnj969  29415  bnj1463  29522  4atlem12  30507  cdleme48fv  31394  cdlemg35  31608  mapd0  32561

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 179  df-an 362