MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jca31 Unicode version

Theorem jca31 520
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
StepHypRef Expression
1 jca31.1 . . 3  |-  ( ph  ->  ps )
2 jca31.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 518 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 jca31.3 . 2  |-  ( ph  ->  th )
53, 4jca 518 1  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  3jca  1132  syl21anc  1181  f1oiso2  5865  oewordri  6606  boxriin  6874  cfsuc  7899  genpcl  8648  ltexprlem5  8680  lemulge11  9634  lediv12a  9665  elnnz  10050  uzindOLD  10122  quoremz  10975  quoremnn0ALT  10977  fldiv  10980  leexp1a  11176  faclbnd6  11328  setcinv  13938  dvdsrz  16456  cncnp2  17026  vitalilem1  18979  aaliou3lem2  19739  pntibndlem2  20756  grpoidinv  20891  isrngod  21062  nmcvcn  21284  leopmul  22730  ballotlemfc0  23067  ballotlemfcc  23068  poseq  24324  ax5seg  24638  btwnconn1  24796  islimrs4  25685  finminlem  26334  lzenom  26952  jm2.27c  27203  wallispilem3  27919  wallispilem4  27920  stirlinglem5  27930  constr3lem4  28393  2pm13.193  28617  paddasslem4  30634  cdleme21h  31145  cdleme26eALTN  31172  cdleme40m  31278  cdlemf2  31373  dicssdvh  31998  dihopelvalcpre  32060  dihmeetlem4preN  32118  dih1dimatlem0  32140
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 177  df-an 360
  Copyright terms: Public domain W3C validator