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  5877  exmidapne  7343  nnnq0lem1  7530  prmuloc  7650  suplocexprlemex  7806  prsrlem1  7826  apreap  8631  lemulge11  8910  elnnz  9353  supinfneg  9686  infsupneg  9687  leexp1a  10703  faclbnd6  10853  zfz1isolem1  10949  oddpwdclemdc  12366  ennnfonelemf1  12660  grpidinv2  13260  rhmopp  13808  dvdsrzring  14235  cncnp2m  14551  bj-charfun  15537