ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jca32 Unicode version

Theorem jca32 293
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 290 . 2  |-  ( ph  ->  ( ch  /\  th ) )
51, 4jca 290 1  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  syl12anc  1133  euan  1956  imadiflem  4978  ltexnqq  6506  enq0sym  6530  enq0tr  6532  addclpr  6635  mulclpr  6670  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  lemul12a  7828  fzass4  8925  elfz1b  8952  4fvwrd4  8997  leexp1a  9309  sqrt0rlem  9601
  Copyright terms: Public domain W3C validator