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

Theorem jca32 521
Description: Join three consequents. (Contributed by FL, 1-Aug-2009.)
Hypotheses
Ref Expression
jca31.1  |-  ( ph  ->  ps )
jca31.2  |-  ( ph  ->  ch )
jca31.3  |-  ( ph  ->  th )
Assertion
Ref Expression
jca32  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )

Proof of Theorem jca32
StepHypRef Expression
1 jca31.1 . 2  |-  ( ph  ->  ps )
2 jca31.2 . . 3  |-  ( ph  ->  ch )
3 jca31.3 . . 3  |-  ( ph  ->  th )
42, 3jca 518 . 2  |-  ( ph  ->  ( ch  /\  th ) )
51, 4jca 518 1  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  syl12anc  1181  euan  2274  sbthlem9  7122  nqerf  8701  lemul12a  9761  lediv12a  9796  fzass4  10982  4fvwrd4  11011  leexp1a  11325  mreexexlem2d  13757  islmodd  15843  istps2OLD  16876  restnlly  17425  llyrest  17428  llyidm  17431  uptx  17536  alexsubALTlem2  17955  alexsubALTlem4  17957  ivthlem3  19028  grpoidinv  21186  pjnmopi  23041  cdj1i  23326  dya2iocnrect  24094  probun  24125  erdszelem7  24331  rellyscon  24385  relexpadd  24622  rtrclreclem.min  24631  ax5seg  25308  axcontlem4  25337  segconeq  25375  ifscgr  25409  btwnconn1lem13  25464  btwnconn1lem14  25465  outsideofeq  25495  ellines  25517  itg2gt0cn  25678  frinfm  25923  heiborlem3  26043  isfldidl  26199  mzpincl  26318  mzpindd  26330  diophin  26358  pellexlem3  26422  pellexlem5  26424  wallispilem1  27320  reuan  27464  bnj969  28742  bnj1463  28849  4atlem12  29872  cdleme48fv  30759  cdlemg35  30973  mapd0  31926
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator