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  1167  syl21anbrc  1172  syl21anc  1227  f1oiso2  5795  nnnq0lem1  7387  prmuloc  7507  suplocexprlemex  7663  prsrlem1  7683  apreap  8485  lemulge11  8761  elnnz  9201  supinfneg  9533  infsupneg  9534  leexp1a  10510  faclbnd6  10657  zfz1isolem1  10753  oddpwdclemdc  12105  ennnfonelemf1  12351  cncnp2m  12871  bj-charfun  13689