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  9194  elfzd  10429  fzass4  10478  elfz1b  10507  4fvwrd4  10557  infssfzcldc  10679  infssfzledc  10680  leexp1a  11044  wrd2ind  11509  sqrt0rlem  11783  reumodprminv  13052  islmodd  14678  uptx  15424  distspace  15485  xmetxpbl  15658  pellexlem3  16150  bj-charfundc  16932