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  5460  domssr  7064  supelti  7342  ltexnqq  7775  enq0sym  7799  enq0tr  7801  addclpr  7904  mulclpr  7939  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  suplocexprlemloc  8088  lemul12a  9192  elfzd  10419  fzass4  10468  elfz1b  10497  4fvwrd4  10547  infssfzcldc  10669  infssfzledc  10670  leexp1a  11031  wrd2ind  11495  sqrt0rlem  11769  reumodprminv  13032  islmodd  14629  uptx  15375  distspace  15436  xmetxpbl  15609  pellexlem3  16093  bj-charfundc  16834