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

Theorem jca31 302
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 300 . 2 (𝜑 → (𝜓𝜒))
4 jca31.3 . 2 (𝜑𝜃)
53, 4jca 300 1 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  3jca  1123  syl21anc  1173  f1oiso2  5606  nnnq0lem1  7003  prmuloc  7123  prsrlem1  7286  apreap  8062  lemulge11  8325  elnnz  8758  supinfneg  9081  infsupneg  9082  leexp1a  10006  faclbnd6  10148  zfz1isolem1  10241  oddpwdclemdc  11425
  Copyright terms: Public domain W3C validator