Theorem jca32 308

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 304	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 304	1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  syl12anc  1218  euan  2062  imadiflem  5249  supelti  6946  ltexnqq  7328  enq0sym  7352  enq0tr  7354  addclpr  7457  mulclpr  7492  ltexprlemopl  7521  ltexprlemlol  7522  ltexprlemopu  7523  ltexprlemupu  7524  suplocexprlemloc  7641  lemul12a  8733  fzass4  9964  elfz1b  9992  4fvwrd4  10039  leexp1a  10474  sqrt0rlem  10903  reumodprminv  12128  uptx  12685  distspace  12746  xmetxpbl  12919  bj-charfundc  13394