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

Theorem jca31 536
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 534 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 jca31.3 . 2  |-  ( ph  ->  th )
53, 4jca 534 1  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  3jca  1185  syl21anc  1263  xpdifid  5222  tpres  6071  f1oiso2  6197  oewordri  7243  boxriin  7514  cantnfrescl  8128  cfsuc  8633  genpcl  9379  ltexprlem5  9411  prsrlem1  9442  lemulge11  10413  lediv12a  10445  elnnz  10893  quoremz  12027  quoremnn0ALT  12029  fldiv  12032  leexp1a  12276  faclbnd6  12429  wrdlen2i  12960  wwlktovfo  12972  setcinv  15923  sgrp2rid2  16598  mhmfmhm  16747  gsumval3lem1  17477  dvdsrzring  18989  scmatmhm  19496  cncnp2  20234  vitalilem1  22503  aaliou3lem2  23236  pntibndlem2  24366  iscgrglt  24496  islnoppd  24719  oppcom  24723  opphllem1  24726  opphllem2  24727  opphllem5  24730  oppperpex  24732  hpgerlem  24744  colopp  24748  colhp  24749  ax5seg  24905  constr3lem4  25312  wlknwwlknsur  25377  wlkiswwlksur  25384  frgrancvvdeqlem4  25698  usg2spot2nb  25730  grpoidinv  25873  isrngod  26044  nmcvcn  26268  leopmul  27724  resf1o  28260  rhmopp  28529  oddpwdc  29134  poseq  30437  btwnconn1  30812  finminlem  30918  bj-elid3  31548  ptrecube  31847  poimirlem22  31869  paddasslem4  33300  cdleme21h  33813  cdleme26eALTN  33840  cdleme40m  33946  cdlemf2  34041  dicssdvh  34666  dihopelvalcpre  34728  dihmeetlem4preN  34786  dih1dimatlem0  34808  lzenom  35524  jm2.27c  35775  clrellem  36142  2pm13.193  36832  disjxp1  37327  mullimc  37579  mullimcf  37586  addlimc  37612  0ellimcdiv  37613  cncfshift  37634  cncfperiod  37639  icccncfext  37648  stoweidlem52  37796  wallispilem4  37813  fourierdlem16  37868  fourierdlem21  37873  fourierdlem48  37901  fourierdlem51  37904  fourierdlem52  37905  fourierdlem54  37907  fourierdlem64  37917  fourierdlem76  37929  fourierdlem77  37930  fourierdlem80  37933  fourierdlem86  37939  fourierdlem87  37940  fourierdlem102  37955  fourierdlem114  37967  sge0f1o  38075  sge0split  38102  ismea  38140  nnfoctbdjlem  38144  iundjiun  38149  ismeannd  38156  psmeasure  38160  isomennd  38203  hoidmvle  38269  oexpnegnz  38620  nbupgrres  39174  usgra2pthlem1  39258  rngcinv  39574  rngcinvALTV  39586  ringcinv  39625  ringcinvALTV  39649
  Copyright terms: Public domain W3C validator