Theorem jca31 309

Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
jca31.1	⊢ (𝜑 → 𝜓)
jca31.2	⊢ (𝜑 → 𝜒)
jca31.3	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
jca31	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

Proof of Theorem jca31

Step	Hyp	Ref	Expression
1		jca31.1	. . 3 ⊢ (𝜑 → 𝜓)
2		jca31.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 306	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		jca31.3	. 2 ⊢ (𝜑 → 𝜃)
5	3, 4	jca 306	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  3jca  1208  syl21anbrc  1213  syl21anc  1277  f1oiso2  6036  exmidapne  7632  nnnq0lem1  7819  prmuloc  7939  suplocexprlemex  8095  prsrlem1  8115  apreap  8923  lemulge11  9204  elnnz  9665  supinfneg  10011  infsupneg  10012  leexp1a  11052  faclbnd6  11204  zfz1isolem1  11314  nnmaxpwlemparts  12977  ennnfonelemf1  13367  grpidinv2  13922  rhmopp  14592  dvdsrzring  15047  cncnp2m  15457  upgrex  16549  uhgr2edg  16652  bj-charfun  17038