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

Theorem jca31 521
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 519 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 jca31.3 . 2  |-  ( ph  ->  th )
53, 4jca 519 1  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  3jca  1134  syl21anc  1183  f1oiso2  6072  oewordri  6835  boxriin  7104  cfsuc  8137  genpcl  8885  ltexprlem5  8917  lemulge11  9872  lediv12a  9903  elnnz  10292  uzindOLD  10364  quoremz  11236  quoremnn0ALT  11238  fldiv  11241  leexp1a  11438  faclbnd6  11590  setcinv  14245  dvdsrz  16767  cncnp2  17345  vitalilem1  19500  aaliou3lem2  20260  pntibndlem2  21285  constr3lem4  21634  grpoidinv  21796  isrngod  21967  nmcvcn  22191  leopmul  23637  rhmopp  24257  poseq  25528  ax5seg  25877  btwnconn1  26035  finminlem  26321  lzenom  26828  jm2.27c  27078  stoweidlem52  27777  wallispilem4  27793  usgra2pthlem1  28310  frgrancvvdeqlem4  28422  usg2spot2nb  28454  2pm13.193  28639  paddasslem4  30620  cdleme21h  31131  cdleme26eALTN  31158  cdleme40m  31264  cdlemf2  31359  dicssdvh  31984  dihopelvalcpre  32046  dihmeetlem4preN  32104  dih1dimatlem0  32126
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
  Copyright terms: Public domain W3C validator