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

Theorem jca32 306
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 302 . 2  |-  ( ph  ->  ( ch  /\  th ) )
51, 4jca 302 1  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107
This theorem is referenced by:  syl12anc  1197  euan  2031  imadiflem  5160  supelti  6841  ltexnqq  7164  enq0sym  7188  enq0tr  7190  addclpr  7293  mulclpr  7328  ltexprlemopl  7357  ltexprlemlol  7358  ltexprlemopu  7359  ltexprlemupu  7360  lemul12a  8530  fzass4  9735  elfz1b  9763  4fvwrd4  9810  leexp1a  10241  sqrt0rlem  10667  uptx  12285  distspace  12324  xmetxpbl  12497
  Copyright terms: Public domain W3C validator