Theorem jca31 307

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 304	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		jca31.3	. 2 ⊢ (𝜑 → 𝜃)
5	3, 4	jca 304	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  3jca  1172  syl21anbrc  1177  syl21anc  1232  f1oiso2  5806  nnnq0lem1  7408  prmuloc  7528  suplocexprlemex  7684  prsrlem1  7704  apreap  8506  lemulge11  8782  elnnz  9222  supinfneg  9554  infsupneg  9555  leexp1a  10531  faclbnd6  10678  zfz1isolem1  10775  oddpwdclemdc  12127  ennnfonelemf1  12373  grpidinv2  12758  cncnp2m  13025  bj-charfun  13842