Theorem jca32 522

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  syl12anc  1182  euan  2315  sbthlem9  7188  nqerf  8767  lemul12a  9828  lediv12a  9863  fzass4  11050  4fvwrd4  11080  leexp1a  11397  mreexexlem2d  13829  islmodd  15915  istps2OLD  16945  neitr  17202  restnlly  17502  llyrest  17505  llyidm  17508  uptx  17614  alexsubALTlem2  18036  alexsubALTlem4  18038  ivthlem3  19307  grpoidinv  21753  pjnmopi  23608  cdj1i  23893  xrofsup  24083  dya2iocnrect  24588  sitgfval  24612  erdszelem7  24840  rellyscon  24895  relexpadd  25095  rtrclreclem.min  25104  ax5seg  25785  axcontlem4  25814  segconeq  25852  ifscgr  25886  btwnconn1lem13  25941  btwnconn1lem14  25942  outsideofeq  25972  ellines  25994  itg2gt0cn  26163  frinfm  26331  heiborlem3  26416  isfldidl  26572  mzpincl  26685  mzpindd  26697  diophin  26725  pellexlem3  26788  pellexlem5  26790  stoweidlem1  27621  stoweidlem3  27623  stoweidlem14  27634  stoweidlem17  27637  stoweidlem57  27677  reuan  27829  swrdccatin12c  28032  usg2spot2nb  28172  bnj969  29027  bnj1463  29134  4atlem12  30098  cdleme48fv  30985  cdlemg35  31199  mapd0  32152

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361