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

Theorem jca32 308
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 304 . 2 (𝜑 → (𝜒𝜃))
51, 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:  syl12anc  1218  euan  2062  imadiflem  5249  supelti  6946  ltexnqq  7328  enq0sym  7352  enq0tr  7354  addclpr  7457  mulclpr  7492  ltexprlemopl  7521  ltexprlemlol  7522  ltexprlemopu  7523  ltexprlemupu  7524  suplocexprlemloc  7641  lemul12a  8733  fzass4  9964  elfz1b  9992  4fvwrd4  10039  leexp1a  10474  sqrt0rlem  10903  reumodprminv  12128  uptx  12685  distspace  12746  xmetxpbl  12919  bj-charfundc  13394
  Copyright terms: Public domain W3C validator