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

Theorem jca31 532
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 530 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 jca31.3 . 2  |-  ( ph  ->  th )
53, 4jca 530 1  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  3jca  1174  syl21anc  1225  xpdifid  5420  tpres  6100  f1oiso2  6223  oewordri  7233  boxriin  7504  cantnfrescl  8086  cfsuc  8628  genpcl  9375  ltexprlem5  9407  prsrlem1  9438  lemulge11  10400  lediv12a  10433  elnnz  10870  uzindOLD  10953  quoremz  11964  quoremnn0ALT  11966  fldiv  11969  leexp1a  12209  faclbnd6  12362  wrdlen2i  12878  wwlktovfo  12890  setcinv  15571  sgrp2rid2  16246  mhmfmhm  16395  gsumval3lem1  17111  dvdsrzring  18699  scmatmhm  19206  cncnp2  19952  vitalilem1  22186  aaliou3lem2  22908  pntibndlem2  23977  oppcom  24320  opphllem1  24323  opphllem2  24324  opphllem5  24327  hpgerlem  24338  ax5seg  24446  constr3lem4  24852  wlknwwlknsur  24917  wlkiswwlksur  24924  frgrancvvdeqlem4  25238  usg2spot2nb  25270  grpoidinv  25411  isrngod  25582  nmcvcn  25806  leopmul  27254  resf1o  27787  rhmopp  28047  oddpwdc  28560  poseq  29576  btwnconn1  29982  finminlem  30379  lzenom  30945  jm2.27c  31191  mullimc  31864  mullimcf  31871  addlimc  31896  0ellimcdiv  31897  cncfshift  31918  cncfperiod  31923  icccncfext  31932  stoweidlem52  32076  wallispilem4  32092  fourierdlem16  32147  fourierdlem21  32152  fourierdlem48  32179  fourierdlem51  32182  fourierdlem52  32183  fourierdlem54  32185  fourierdlem64  32195  fourierdlem76  32207  fourierdlem77  32208  fourierdlem80  32211  fourierdlem86  32217  fourierdlem87  32218  fourierdlem102  32233  fourierdlem114  32245  oexpnegnz  32592  usgra2pthlem1  32744  rngcinv  33062  rngcinvALTV  33074  ringcinv  33113  ringcinvALTV  33137  2pm13.193  33738  bj-elid3  35021  paddasslem4  35963  cdleme21h  36476  cdleme26eALTN  36503  cdleme40m  36609  cdlemf2  36704  dicssdvh  37329  dihopelvalcpre  37391  dihmeetlem4preN  37449  dih1dimatlem0  37471
  Copyright terms: Public domain W3C validator