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

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

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