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  1276  euan  2143  imadiflem  5455  domssr  7054  supelti  7332  ltexnqq  7765  enq0sym  7789  enq0tr  7791  addclpr  7894  mulclpr  7929  ltexprlemopl  7958  ltexprlemlol  7959  ltexprlemopu  7960  ltexprlemupu  7961  suplocexprlemloc  8078  lemul12a  9182  elfzd  10398  fzass4  10446  elfz1b  10475  4fvwrd4  10525  infssfzcldc  10647  infssfzledc  10648  leexp1a  11009  wrd2ind  11473  sqrt0rlem  11747  reumodprminv  13010  islmodd  14602  uptx  15298  distspace  15359  xmetxpbl  15532  pellexlem3  16007  bj-charfundc  16748