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  1214  euan  2055  imadiflem  5202  supelti  6889  ltexnqq  7216  enq0sym  7240  enq0tr  7242  addclpr  7345  mulclpr  7380  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  suplocexprlemloc  7529  lemul12a  8620  fzass4  9842  elfz1b  9870  4fvwrd4  9917  leexp1a  10348  sqrt0rlem  10775  uptx  12443  distspace  12504  xmetxpbl  12677
 Copyright terms: Public domain W3C validator