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  5950  exmidapne  7442  nnnq0lem1  7629  prmuloc  7749  suplocexprlemex  7905  prsrlem1  7925  apreap  8730  lemulge11  9009  elnnz  9452  supinfneg  9786  infsupneg  9787  leexp1a  10811  faclbnd6  10961  zfz1isolem1  11057  oddpwdclemdc  12690  ennnfonelemf1  12984  grpidinv2  13586  rhmopp  14134  dvdsrzring  14561  cncnp2m  14899  upgrex  15897  uhgr2edg  15998  bj-charfun  16128