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  1248  euan  2111  imadiflem  5361  domssr  6881  supelti  7118  ltexnqq  7536  enq0sym  7560  enq0tr  7562  addclpr  7665  mulclpr  7700  ltexprlemopl  7729  ltexprlemlol  7730  ltexprlemopu  7731  ltexprlemupu  7732  suplocexprlemloc  7849  lemul12a  8950  elfzd  10153  fzass4  10199  elfz1b  10227  4fvwrd4  10277  leexp1a  10756  wrd2ind  11194  sqrt0rlem  11384  reumodprminv  12646  islmodd  14125  uptx  14816  distspace  14877  xmetxpbl  15050  bj-charfundc  15878