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  1208  syl21anbrc  1213  syl21anc  1277  f1oiso2  6023  exmidapne  7616  nnnq0lem1  7803  prmuloc  7923  suplocexprlemex  8079  prsrlem1  8099  apreap  8905  lemulge11  9186  elnnz  9633  supinfneg  9974  infsupneg  9975  leexp1a  11009  faclbnd6  11160  zfz1isolem1  11270  oddpwdclemdc  12929  ennnfonelemf1  13287  grpidinv2  13840  rhmopp  14456  dvdsrzring  14910  cncnp2m  15255  upgrex  16258  uhgr2edg  16361  bj-charfun  16747