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

Theorem jca32 310
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 306 . 2  |-  ( ph  ->  ( ch  /\  th ) )
51, 4jca 306 1  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  syl12anc  1247  euan  2094  imadiflem  5314  supelti  7030  ltexnqq  7436  enq0sym  7460  enq0tr  7462  addclpr  7565  mulclpr  7600  ltexprlemopl  7629  ltexprlemlol  7630  ltexprlemopu  7631  ltexprlemupu  7632  suplocexprlemloc  7749  lemul12a  8848  elfzd  10045  fzass4  10091  elfz1b  10119  4fvwrd4  10169  leexp1a  10605  sqrt0rlem  11043  reumodprminv  12284  islmodd  13606  uptx  14226  distspace  14287  xmetxpbl  14460  bj-charfundc  15013
  Copyright terms: Public domain W3C validator