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  1271  euan  2136  imadiflem  5409  domssr  6950  supelti  7200  ltexnqq  7627  enq0sym  7651  enq0tr  7653  addclpr  7756  mulclpr  7791  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  suplocexprlemloc  7940  lemul12a  9041  elfzd  10250  fzass4  10296  elfz1b  10324  4fvwrd4  10374  leexp1a  10855  wrd2ind  11303  sqrt0rlem  11563  reumodprminv  12825  islmodd  14306  uptx  14997  distspace  15058  xmetxpbl  15231  bj-charfundc  16403