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

Theorem jca32 308
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 304 . 2  |-  ( ph  ->  ( ch  /\  th ) )
51, 4jca 304 1  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  syl12anc  1215  euan  2056  imadiflem  5209  supelti  6896  ltexnqq  7239  enq0sym  7263  enq0tr  7265  addclpr  7368  mulclpr  7403  ltexprlemopl  7432  ltexprlemlol  7433  ltexprlemopu  7434  ltexprlemupu  7435  suplocexprlemloc  7552  lemul12a  8643  fzass4  9872  elfz1b  9900  4fvwrd4  9947  leexp1a  10378  sqrt0rlem  10806  uptx  12480  distspace  12541  xmetxpbl  12714
  Copyright terms: Public domain W3C validator