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

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

Proof of Theorem jca32
StepHypRef Expression
1 jca31.1 . 2 (𝜑𝜓)
2 jca31.2 . . 3 (𝜑𝜒)
3 jca31.3 . . 3 (𝜑𝜃)
42, 3jca 290 . 2 (𝜑 → (𝜒𝜃))
51, 4jca 290 1 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101 This theorem is referenced by:  syl12anc  1133  euan  1956  imadiflem  4978  ltexnqq  6506  enq0sym  6530  enq0tr  6532  addclpr  6635  mulclpr  6670  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  lemul12a  7828  fzass4  8925  elfz1b  8952  4fvwrd4  8997  leexp1a  9309  sqrt0rlem  9601
 Copyright terms: Public domain W3C validator