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  5400  domssr  6937  supelti  7180  ltexnqq  7606  enq0sym  7630  enq0tr  7632  addclpr  7735  mulclpr  7770  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  suplocexprlemloc  7919  lemul12a  9020  elfzd  10224  fzass4  10270  elfz1b  10298  4fvwrd4  10348  leexp1a  10828  wrd2ind  11270  sqrt0rlem  11529  reumodprminv  12791  islmodd  14272  uptx  14963  distspace  15024  xmetxpbl  15197  bj-charfundc  16226