ILE Home 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  6504  enq0sym  6528  enq0tr  6530  addclpr  6633  mulclpr  6668  ltexprlemopl  6697  ltexprlemlol  6698  ltexprlemopu  6699  ltexprlemupu  6700  lemul12a  7826  fzass4  8923  elfz1b  8950  4fvwrd4  8995  leexp1a  9307  sqrt0rlem  9599
  Copyright terms: Public domain W3C validator