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

Theorem jca31 543
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 541 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 jca31.3 . 2  |-  ( ph  ->  th )
53, 4jca 541 1  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  3jca  1210  syl21anc  1291  xpdifid  5271  tpres  6133  f1oiso2  6261  oewordri  7311  boxriin  7582  cantnfrescl  8199  cfsuc  8705  genpcl  9451  ltexprlem5  9483  prsrlem1  9514  lemulge11  10489  lediv12a  10521  elnnz  10971  quoremz  12115  quoremnn0ALT  12117  fldiv  12120  modsumfzodifsn  12196  leexp1a  12369  faclbnd6  12522  wrdlen2i  13093  wwlktovfo  13108  setcinv  16063  sgrp2rid2  16738  mhmfmhm  16887  gsumval3lem1  17617  dvdsrzring  19129  scmatmhm  19636  cncnp2  20374  vitalilem1  22645  aaliou3lem2  23378  pntibndlem2  24508  iscgrglt  24638  islnoppd  24861  oppcom  24865  opphllem1  24868  opphllem2  24869  opphllem5  24872  oppperpex  24874  hpgerlem  24886  colopp  24890  colhp  24891  ax5seg  25047  constr3lem4  25454  wlknwwlknsur  25519  wlkiswwlksur  25526  frgrancvvdeqlem4  25840  usg2spot2nb  25872  grpoidinv  26017  isrngod  26188  nmcvcn  26412  leopmul  27868  resf1o  28390  rhmopp  28656  oddpwdc  29260  poseq  30562  btwnconn1  30939  finminlem  31045  bj-elid3  31712  ptrecube  32004  poimirlem22  32026  paddasslem4  33459  cdleme21h  33972  cdleme26eALTN  33999  cdleme40m  34105  cdlemf2  34200  dicssdvh  34825  dihopelvalcpre  34887  dihmeetlem4preN  34945  dih1dimatlem0  34967  lzenom  35683  jm2.27c  35933  clrellem  36300  2pm13.193  36989  disjxp1  37470  infleinflem2  37681  mullimc  37793  mullimcf  37800  addlimc  37826  0ellimcdiv  37827  cncfshift  37848  cncfperiod  37853  icccncfext  37862  stoweidlem52  38025  wallispilem4  38042  fourierdlem16  38097  fourierdlem21  38102  fourierdlem48  38130  fourierdlem51  38133  fourierdlem52  38134  fourierdlem54  38136  fourierdlem64  38146  fourierdlem76  38158  fourierdlem77  38159  fourierdlem80  38162  fourierdlem86  38168  fourierdlem87  38169  fourierdlem102  38184  fourierdlem114  38196  sge0f1o  38338  sge0split  38365  ismea  38405  nnfoctbdjlem  38409  iundjiun  38414  ismeannd  38421  psmeasure  38425  isomennd  38471  hoidmvle  38540  ovncvr2  38551  oexpnegnz  38952  uhgr2edg  39453  nbupgrres  39602  crctcsh1wlkn0lem5  39992  1pthond  40032  3pthdlem1  40078  usgra2pthlem1  40175  rngcinv  40491  rngcinvALTV  40503  ringcinv  40542  ringcinvALTV  40566
  Copyright terms: Public domain W3C validator