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  7070  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  10435  fzass4  10484  elfz1b  10513  4fvwrd4  10563  infssfzcldc  10685  infssfzledc  10686  leexp1a  11051  wrd2ind  11516  sqrt0rlem  11790  reumodprminv  13060  islmodd  14737  psrbagmax  15183  uptx  15517  distspace  15578  xmetxpbl  15751  pellexlem3  16248  bj-charfundc  17056