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  1201  syl21anbrc  1206  syl21anc  1270  f1oiso2  5957  exmidapne  7457  nnnq0lem1  7644  prmuloc  7764  suplocexprlemex  7920  prsrlem1  7940  apreap  8745  lemulge11  9024  elnnz  9467  supinfneg  9802  infsupneg  9803  leexp1a  10828  faclbnd6  10978  zfz1isolem1  11075  oddpwdclemdc  12710  ennnfonelemf1  13004  grpidinv2  13606  rhmopp  14155  dvdsrzring  14582  cncnp2m  14920  upgrex  15918  uhgr2edg  16019  bj-charfun  16225