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  1215  euan  2056  imadiflem  5210  supelti  6897  ltexnqq  7240  enq0sym  7264  enq0tr  7266  addclpr  7369  mulclpr  7404  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  suplocexprlemloc  7553  lemul12a  8644  fzass4  9873  elfz1b  9901  4fvwrd4  9948  leexp1a  10379  sqrt0rlem  10807  uptx  12482  distspace  12543  xmetxpbl  12716