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  1179  syl21anbrc  1184  syl21anc  1248  f1oiso2  5871  exmidapne  7322  nnnq0lem1  7508  prmuloc  7628  suplocexprlemex  7784  prsrlem1  7804  apreap  8608  lemulge11  8887  elnnz  9330  supinfneg  9663  infsupneg  9664  leexp1a  10668  faclbnd6  10818  zfz1isolem1  10914  oddpwdclemdc  12314  ennnfonelemf1  12578  grpidinv2  13133  rhmopp  13675  dvdsrzring  14102  cncnp2m  14410  bj-charfun  15369