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

Theorem jca31 534
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 532 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 jca31.3 . 2  |-  ( ph  ->  th )
53, 4jca 532 1  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  3jca  1168  syl21anc  1217  f1oiso2  6038  oewordri  7023  boxriin  7297  cantnfrescl  7876  cfsuc  8418  genpcl  9169  ltexprlem5  9201  lemulge11  10183  lediv12a  10217  elnnz  10648  uzindOLD  10728  quoremz  11686  quoremnn0ALT  11688  fldiv  11691  leexp1a  11914  faclbnd6  12067  wrdlen2i  12538  setcinv  14950  gsumval3lem1  16374  dvdsrzring  17876  dvdsrz  17877  cncnp2  18860  vitalilem1  21063  aaliou3lem2  21784  pntibndlem2  22815  ax5seg  23135  constr3lem4  23484  grpoidinv  23646  isrngod  23817  nmcvcn  24041  leopmul  25489  resf1o  25981  rhmopp  26238  oddpwdc  26689  poseq  27665  btwnconn1  28083  finminlem  28466  lzenom  29061  jm2.27c  29309  stoweidlem52  29800  wallispilem4  29816  wwlktovfo  30206  usgra2pthlem1  30253  wlknwwlknsur  30297  wlkiswwlksur  30304  frgrancvvdeqlem4  30579  usg2spot2nb  30611  2pm13.193  31148  paddasslem4  33307  cdleme21h  33818  cdleme26eALTN  33845  cdleme40m  33951  cdlemf2  34046  dicssdvh  34671  dihopelvalcpre  34733  dihmeetlem4preN  34791  dih1dimatlem0  34813
  Copyright terms: Public domain W3C validator