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

Theorem jca31 303
Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
jca31.1 (𝜑𝜓)
jca31.2 (𝜑𝜒)
jca31.3 (𝜑𝜃)
Assertion
Ref Expression
jca31 (𝜑 → ((𝜓𝜒) ∧ 𝜃))

Proof of Theorem jca31
StepHypRef Expression
1 jca31.1 . . 3 (𝜑𝜓)
2 jca31.2 . . 3 (𝜑𝜒)
31, 2jca 301 . 2 (𝜑 → (𝜓𝜒))
4 jca31.3 . 2 (𝜑𝜃)
53, 4jca 301 1 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
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:  3jca  1124  syl21anc  1174  f1oiso2  5620  nnnq0lem1  7066  prmuloc  7186  prsrlem1  7349  apreap  8125  lemulge11  8388  elnnz  8821  supinfneg  9144  infsupneg  9145  leexp1a  10071  faclbnd6  10213  zfz1isolem1  10306  oddpwdclemdc  11490
  Copyright terms: Public domain W3C validator