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  1272  euan  2139  imadiflem  5440  domssr  7030  supelti  7306  ltexnqq  7739  enq0sym  7763  enq0tr  7765  addclpr  7868  mulclpr  7903  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  suplocexprlemloc  8052  lemul12a  9153  elfzd  10369  fzass4  10417  elfz1b  10446  4fvwrd4  10496  infssfzcldc  10618  infssfzledc  10619  leexp1a  10980  wrd2ind  11440  sqrt0rlem  11713  reumodprminv  12976  islmodd  14567  uptx  15265  distspace  15326  xmetxpbl  15499  pellexlem3  15973  bj-charfundc  16704