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  1176  syl21anc  1227  f1oiso2  6247  oewordri  7253  boxriin  7523  cantnfrescl  8107  cfsuc  8649  genpcl  9398  ltexprlem5  9430  prsrlem1  9461  lemulge11  10416  lediv12a  10450  elnnz  10886  uzindOLD  10967  quoremz  11962  quoremnn0ALT  11964  fldiv  11967  leexp1a  12204  faclbnd6  12357  wrdlen2i  12864  wwlktovfo  12876  setcinv  15292  sgrp2rid2  15916  mhmfmhm  16065  ghmfghm  16712  gsumval3lem1  16782  dvdsrzring  18376  dvdsrz  18377  scmatmhm  18905  cncnp2  19650  vitalilem1  21885  aaliou3lem2  22606  pntibndlem2  23642  oppcom  23958  opphllem1  23959  opphllem2  23960  ax5seg  24064  constr3lem4  24470  wlknwwlknsur  24535  wlkiswwlksur  24542  frgrancvvdeqlem4  24857  usg2spot2nb  24889  grpoidinv  25033  isrngod  25204  nmcvcn  25428  leopmul  26876  resf1o  27376  rhmopp  27634  oddpwdc  28118  poseq  29260  btwnconn1  29678  finminlem  30063  lzenom  30631  jm2.27c  30877  ioondisj2  31412  ioondisj1  31413  mullimc  31481  islptre  31484  mullimcf  31488  limcrecl  31494  lptioo2  31496  lptioo1  31497  addlimc  31513  0ellimcdiv  31514  cncfshift  31535  cncfperiod  31540  icccncfext  31549  cncfiooicclem1  31555  stoweidlem52  31675  wallispilem4  31691  fourierdlem16  31746  fourierdlem21  31751  fourierdlem48  31778  fourierdlem52  31782  fourierdlem54  31784  fourierdlem64  31794  fourierdlem76  31806  fourierdlem77  31807  fourierdlem80  31810  fourierdlem86  31816  fourierdlem87  31817  fourierdlem102  31832  fourierdlem114  31844  usgra2pthlem1  32143  ringcinv  32372  2pm13.193  32806  paddasslem4  35020  cdleme21h  35531  cdleme26eALTN  35558  cdleme40m  35664  cdlemf2  35759  dicssdvh  36384  dihopelvalcpre  36446  dihmeetlem4preN  36504  dih1dimatlem0  36526
  Copyright terms: Public domain W3C validator