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

Theorem jca31 307
 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 304 . 2 (𝜑 → (𝜓𝜒))
4 jca31.3 . 2 (𝜑𝜃)
53, 4jca 304 1 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
 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  1161  syl21anc  1215  f1oiso2  5721  nnnq0lem1  7247  prmuloc  7367  suplocexprlemex  7523  prsrlem1  7543  apreap  8342  lemulge11  8617  elnnz  9057  supinfneg  9383  infsupneg  9384  leexp1a  10341  faclbnd6  10483  zfz1isolem1  10576  oddpwdclemdc  11840  ennnfonelemf1  11920  cncnp2m  12389
 Copyright terms: Public domain W3C validator