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  9663  supinfneg  10010  infsupneg  10011  leexp1a  11051  faclbnd6  11203  zfz1isolem1  11313  nnmaxpwlemparts  12976  ennnfonelemf1  13366  grpidinv2  13921  rhmopp  14591  dvdsrzring  15046  cncnp2m  15474  upgrex  16566  uhgr2edg  16669  bj-charfun  17055