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  1226  euan  2070  imadiflem  5266  supelti  6963  ltexnqq  7345  enq0sym  7369  enq0tr  7371  addclpr  7474  mulclpr  7509  ltexprlemopl  7538  ltexprlemlol  7539  ltexprlemopu  7540  ltexprlemupu  7541  suplocexprlemloc  7658  lemul12a  8753  fzass4  9993  elfz1b  10021  4fvwrd4  10071  leexp1a  10506  sqrt0rlem  10941  reumodprminv  12181  uptx  12874  distspace  12935  xmetxpbl  13108  bj-charfundc  13650