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

Theorem jca32 523
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 520 . 2  |-  ( ph  ->  ( ch  /\  th ) )
51, 4jca 520 1  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  syl12anc  1183  euan  2344  sbthlem9  7254  nqerf  8838  lemul12a  9899  lediv12a  9934  fzass4  11121  4fvwrd4  11152  leexp1a  11469  mreexexlem2d  13901  islmodd  15987  istps2OLD  17017  neitr  17275  restnlly  17576  llyrest  17579  llyidm  17582  uptx  17688  alexsubALTlem2  18110  alexsubALTlem4  18112  ivthlem3  19381  grpoidinv  21827  pjnmopi  23682  cdj1i  23967  xrofsup  24157  dya2iocnrect  24662  sitgfval  24686  erdszelem7  24914  rellyscon  24969  relexpadd  25169  rtrclreclem.min  25178  ax5seg  25908  axcontlem4  25937  segconeq  25975  ifscgr  26009  btwnconn1lem13  26064  btwnconn1lem14  26065  outsideofeq  26095  ellines  26117  itg2gt0cn  26298  frinfm  26475  heiborlem3  26560  isfldidl  26716  mzpincl  26829  mzpindd  26841  diophin  26869  pellexlem3  26932  pellexlem5  26934  stoweidlem1  27764  stoweidlem3  27766  stoweidlem14  27777  stoweidlem17  27780  stoweidlem57  27820  reuan  27972  2cshw2lem1  28310  2cshw2lem2  28311  usg2spot2nb  28552  bnj969  29415  bnj1463  29522  4atlem12  30507  cdleme48fv  31394  cdlemg35  31608  mapd0  32561
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 179  df-an 362
  Copyright terms: Public domain W3C validator