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  1180  euan  2200  sbthlem9  6979  nqerf  8554  lemul12a  9614  lediv12a  9649  fzass4  10829  leexp1a  11160  mreexexlem2d  13547  islmodd  15633  istps2OLD  16659  restnlly  17208  llyrest  17211  llyidm  17214  uptx  17319  alexsubALTlem2  17742  alexsubALTlem4  17744  ivthlem3  18813  grpoidinv  20875  pjnmopi  22728  cdj1i  23013  probun  23622  erdszelem7  23728  rellyscon  23782  relexpadd  24035  rtrclreclem.min  24044  ax5seg  24566  axcontlem4  24595  segconeq  24633  ifscgr  24667  btwnconn1lem13  24722  btwnconn1lem14  24723  outsideofeq  24753  ellines  24775  repcpwti  25161  domncnt  25282  bisig0  26062  frinfm  26416  heiborlem3  26537  isfldidl  26693  mzpincl  26812  mzpindd  26824  diophin  26852  pellexlem3  26916  pellexlem5  26918  wallispilem1  27814  reuan  27958  bnj969  28978  bnj1463  29085  4atlem12  29801  cdleme48fv  30688  cdlemg35  30902  mapd0  31855
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