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  5849  oewordri  6590  boxriin  6858  cfsuc  7883  genpcl  8632  ltexprlem5  8664  lemulge11  9618  lediv12a  9649  elnnz  10034  uzindOLD  10106  quoremz  10959  quoremnn0ALT  10961  fldiv  10964  leexp1a  11160  faclbnd6  11312  setcinv  13922  dvdsrz  16440  cncnp2  17010  vitalilem1  18963  aaliou3lem2  19723  pntibndlem2  20740  grpoidinv  20875  isrngod  21046  nmcvcn  21268  leopmul  22714  ballotlemfc0  23051  ballotlemfcc  23052  poseq  24253  ax5seg  24566  btwnconn1  24724  islimrs4  25582  finminlem  26231  lzenom  26849  jm2.27c  27100  wallispilem3  27816  wallispilem4  27817  stirlinglem5  27827  2pm13.193  28318  paddasslem4  30012  cdleme21h  30523  cdleme26eALTN  30550  cdleme40m  30656  cdlemf2  30751  dicssdvh  31376  dihopelvalcpre  31438  dihmeetlem4preN  31496  dih1dimatlem0  31518
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