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  5963  exmidapne  7469  nnnq0lem1  7656  prmuloc  7776  suplocexprlemex  7932  prsrlem1  7952  apreap  8757  lemulge11  9036  elnnz  9479  supinfneg  9819  infsupneg  9820  leexp1a  10846  faclbnd6  10996  zfz1isolem1  11094  oddpwdclemdc  12735  ennnfonelemf1  13029  grpidinv2  13631  rhmopp  14180  dvdsrzring  14607  cncnp2m  14945  upgrex  15944  uhgr2edg  16045  bj-charfun  16338