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 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  syl12anc  1276  euan  2143  imadiflem  5463  domssr  7068  supelti  7348  ltexnqq  7781  enq0sym  7805  enq0tr  7807  addclpr  7910  mulclpr  7945  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  suplocexprlemloc  8094  lemul12a  9200  elfzd  10436  fzass4  10485  elfz1b  10514  4fvwrd4  10564  infssfzcldc  10686  infssfzledc  10687  leexp1a  11052  wrd2ind  11517  sqrt0rlem  11791  reumodprminv  13061  islmodd  14738  uptx  15500  distspace  15561  xmetxpbl  15734  pellexlem3  16231  bj-charfundc  17039