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  1269  euan  2134  imadiflem  5406  domssr  6946  supelti  7192  ltexnqq  7618  enq0sym  7642  enq0tr  7644  addclpr  7747  mulclpr  7782  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  suplocexprlemloc  7931  lemul12a  9032  elfzd  10241  fzass4  10287  elfz1b  10315  4fvwrd4  10365  leexp1a  10846  wrd2ind  11294  sqrt0rlem  11554  reumodprminv  12816  islmodd  14297  uptx  14988  distspace  15049  xmetxpbl  15222  bj-charfundc  16339