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  1269  euan  2134  imadiflem  5399  domssr  6927  supelti  7165  ltexnqq  7591  enq0sym  7615  enq0tr  7617  addclpr  7720  mulclpr  7755  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  suplocexprlemloc  7904  lemul12a  9005  elfzd  10208  fzass4  10254  elfz1b  10282  4fvwrd4  10332  leexp1a  10811  wrd2ind  11250  sqrt0rlem  11509  reumodprminv  12771  islmodd  14251  uptx  14942  distspace  15003  xmetxpbl  15176  bj-charfundc  16129