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  1247  euan  2098  imadiflem  5334  supelti  7063  ltexnqq  7470  enq0sym  7494  enq0tr  7496  addclpr  7599  mulclpr  7634  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  suplocexprlemloc  7783  lemul12a  8883  elfzd  10085  fzass4  10131  elfz1b  10159  4fvwrd4  10209  leexp1a  10668  sqrt0rlem  11150  reumodprminv  12394  islmodd  13792  uptx  14453  distspace  14514  xmetxpbl  14687  bj-charfundc  15370