Theorem jca32 303

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  syl12anc  1167  euan  1997  imadiflem  4998  supelti  6415  ltexnqq  6598  enq0sym  6622  enq0tr  6624  addclpr  6727  mulclpr  6762  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  lemul12a  7940  fzass4  9080  elfz1b  9107  4fvwrd4  9150  leexp1a  9531  sqrt0rlem  9889