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  1231  euan  2075  imadiflem  5277  supelti  6979  ltexnqq  7370  enq0sym  7394  enq0tr  7396  addclpr  7499  mulclpr  7534  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  suplocexprlemloc  7683  lemul12a  8778  fzass4  10018  elfz1b  10046  4fvwrd4  10096  leexp1a  10531  sqrt0rlem  10967  reumodprminv  12207  uptx  13068  distspace  13129  xmetxpbl  13302  bj-charfundc  13843