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  6033  exmidapne  7627  nnnq0lem1  7814  prmuloc  7934  suplocexprlemex  8090  prsrlem1  8110  apreap  8918  lemulge11  9199  elnnz  9659  supinfneg  10005  infsupneg  10006  leexp1a  11046  faclbnd6  11198  zfz1isolem1  11308  nnmaxpwlemparts  12971  ennnfonelemf1  13361  grpidinv2  13916  rhmopp  14567  dvdsrzring  15022  cncnp2m  15423  upgrex  16510  uhgr2edg  16613  bj-charfun  16999