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

Theorem jca32 297
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 294 . 2  |-  ( ph  ->  ( ch  /\  th ) )
51, 4jca 294 1  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  syl12anc  1144  euan  1972  imadiflem  5005  ltexnqq  6563  enq0sym  6587  enq0tr  6589  addclpr  6692  mulclpr  6727  ltexprlemopl  6756  ltexprlemlol  6757  ltexprlemopu  6758  ltexprlemupu  6759  lemul12a  7902  fzass4  9026  elfz1b  9053  4fvwrd4  9098  leexp1a  9469  sqrt0rlem  9822
  Copyright terms: Public domain W3C validator