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  6026  exmidapne  7619  nnnq0lem1  7806  prmuloc  7926  suplocexprlemex  8082  prsrlem1  8102  apreap  8908  lemulge11  9189  elnnz  9636  supinfneg  9977  infsupneg  9978  leexp1a  11012  faclbnd6  11163  zfz1isolem1  11273  oddpwdclemdc  12932  ennnfonelemf1  13290  grpidinv2  13843  rhmopp  14459  dvdsrzring  14913  cncnp2m  15258  upgrex  16261  uhgr2edg  16364  bj-charfun  16750