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

Theorem jca31 307
Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
jca31.1  |-  ( ph  ->  ps )
jca31.2  |-  ( ph  ->  ch )
jca31.3  |-  ( ph  ->  th )
Assertion
Ref Expression
jca31  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)

Proof of Theorem jca31
StepHypRef Expression
1 jca31.1 . . 3  |-  ( ph  ->  ps )
2 jca31.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 304 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 jca31.3 . 2  |-  ( ph  ->  th )
53, 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:  3jca  1146  syl21anc  1200  f1oiso2  5696  nnnq0lem1  7222  prmuloc  7342  suplocexprlemex  7498  prsrlem1  7518  apreap  8317  lemulge11  8592  elnnz  9032  supinfneg  9358  infsupneg  9359  leexp1a  10316  faclbnd6  10458  zfz1isolem1  10551  oddpwdclemdc  11778  ennnfonelemf1  11858  cncnp2m  12327
  Copyright terms: Public domain W3C validator