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  1218  f1oiso2  6155  oewordri  7144  boxriin  7418  cantnfrescl  7998  cfsuc  8540  genpcl  9291  ltexprlem5  9323  lemulge11  10305  lediv12a  10339  elnnz  10770  uzindOLD  10850  quoremz  11814  quoremnn0ALT  11816  fldiv  11819  leexp1a  12042  faclbnd6  12195  wrdlen2i  12667  setcinv  15080  gsumval3lem1  16507  dvdsrzring  18029  dvdsrz  18030  cncnp2  19020  vitalilem1  21224  aaliou3lem2  21945  pntibndlem2  22976  ax5seg  23356  constr3lem4  23705  grpoidinv  23867  isrngod  24038  nmcvcn  24262  leopmul  25710  resf1o  26201  rhmopp  26452  oddpwdc  26901  poseq  27878  btwnconn1  28296  finminlem  28681  lzenom  29276  jm2.27c  29524  stoweidlem52  30015  wallispilem4  30031  wwlktovfo  30421  usgra2pthlem1  30468  wlknwwlknsur  30512  wlkiswwlksur  30519  frgrancvvdeqlem4  30794  usg2spot2nb  30826  2pm13.193  31613  paddasslem4  33825  cdleme21h  34336  cdleme26eALTN  34363  cdleme40m  34469  cdlemf2  34564  dicssdvh  35189  dihopelvalcpre  35251  dihmeetlem4preN  35309  dih1dimatlem0  35331
  Copyright terms: Public domain W3C validator