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

Theorem jca31 309
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 306 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 jca31.3 . 2  |-  ( ph  ->  th )
53, 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:  3jca  1177  syl21anbrc  1182  syl21anc  1237  f1oiso2  5827  exmidapne  7258  nnnq0lem1  7444  prmuloc  7564  suplocexprlemex  7720  prsrlem1  7740  apreap  8542  lemulge11  8821  elnnz  9261  supinfneg  9593  infsupneg  9594  leexp1a  10572  faclbnd6  10719  zfz1isolem1  10815  oddpwdclemdc  12167  ennnfonelemf1  12413  grpidinv2  12922  dvdsrzring  13424  cncnp2m  13662  bj-charfun  14479
  Copyright terms: Public domain W3C validator