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  1236  euan  2082  imadiflem  5294  supelti  6998  ltexnqq  7404  enq0sym  7428  enq0tr  7430  addclpr  7533  mulclpr  7568  ltexprlemopl  7597  ltexprlemlol  7598  ltexprlemopu  7599  ltexprlemupu  7600  suplocexprlemloc  7717  lemul12a  8815  fzass4  10057  elfz1b  10085  4fvwrd4  10135  leexp1a  10570  sqrt0rlem  11005  reumodprminv  12245  uptx  13645  distspace  13706  xmetxpbl  13879  bj-charfundc  14420