Theorem jca32 304

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 301	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 301	1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  syl12anc  1179  euan  2011  imadiflem  5127  supelti  6777  ltexnqq  7064  enq0sym  7088  enq0tr  7090  addclpr  7193  mulclpr  7228  ltexprlemopl  7257  ltexprlemlol  7258  ltexprlemopu  7259  ltexprlemupu  7260  lemul12a  8420  fzass4  9625  elfz1b  9653  4fvwrd4  9700  leexp1a  10141  sqrt0rlem  10567  distspace  12136