Theorem jca32 310

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

Step	Hyp	Ref	Expression
1		jca31.1	. 2 ⊢ (𝜑 → 𝜓)
2		jca31.2	. . 3 ⊢ (𝜑 → 𝜒)
3		jca31.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 306	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 306	1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  syl12anc  1272  euan  2136  imadiflem  5416  domssr  6994  supelti  7244  ltexnqq  7671  enq0sym  7695  enq0tr  7697  addclpr  7800  mulclpr  7835  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  suplocexprlemloc  7984  lemul12a  9084  elfzd  10296  fzass4  10342  elfz1b  10370  4fvwrd4  10420  leexp1a  10902  wrd2ind  11353  sqrt0rlem  11626  reumodprminv  12889  islmodd  14372  uptx  15068  distspace  15129  xmetxpbl  15302  pellexlem3  15776  bj-charfundc  16507