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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

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:  3jca  1203  syl21anbrc  1208  syl21anc  1272  f1oiso2  5968  exmidapne  7479  nnnq0lem1  7666  prmuloc  7786  suplocexprlemex  7942  prsrlem1  7962  apreap  8767  lemulge11  9046  elnnz  9489  supinfneg  9829  infsupneg  9830  leexp1a  10857  faclbnd6  11007  zfz1isolem1  11105  oddpwdclemdc  12750  ennnfonelemf1  13044  grpidinv2  13646  rhmopp  14196  dvdsrzring  14623  cncnp2m  14961  upgrex  15960  uhgr2edg  16063  bj-charfun  16428