Theorem jca31 311

Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
jca31.1	|- (ph -> ps)
jca31.2	|- (ph -> ch)
jca31.3	|- (ph -> th)

Assertion

Ref	Expression
jca31	|- (ph -> ((ps /\ ch) /\ th))

Proof of Theorem jca31

Step	Hyp	Ref	Expression
1		jca31.1	. . 3 |- (ph -> ps)
2		jca31.2	. . 3 |- (ph -> ch)
3	1, 2	jca 310	. 2 |- (ph -> (ps /\ ch))
4		jca31.3	. 2 |- (ph -> th)
5	3, 4	jca 310	1 |- (ph -> ((ps /\ ch) /\ th))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sylan31cOLD 532  3jca 1050  syl21anc 1099  oewordri 5267  xpmapenlem5 5594  genpcl 6263  ltexprlem5 6298  lemulge11 7030  lediv12a 7079  elnnz 7354  uzindOLD 7420  quoremz 7492  quoremnn0 7494  fldiv 7497  expmwordi 7851  sqr2irrlem1 7974  faclbnd 8197  faclbnd6 8206  fsumabs2mul 8304  climmullem8 8387  basgen2 8909  grpidinv 9332  ssga 9455  bnj1001 13366  poseq 13954  cbicplem 14508  fprodadd 14713  curgrpact 14735  cntrsetlem 14999  dualcat2 15133  finminlem 15367  neibastop2lem4 15522  filufint 15574  filnetlem4 15643  fzdisj 15793  bfplem8 16005  phtpyid 16049  phtpyco 16056  reparpht 16065  pcohtpy 16083  pcorev 16087  isringd 16097  grpidinvNEW 17113  paddasslem4 17284

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

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain