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  1177  syl21anbrc  1182  syl21anc  1237  f1oiso2  5830  exmidapne  7261  nnnq0lem1  7447  prmuloc  7567  suplocexprlemex  7723  prsrlem1  7743  apreap  8546  lemulge11  8825  elnnz  9265  supinfneg  9597  infsupneg  9598  leexp1a  10577  faclbnd6  10726  zfz1isolem1  10822  oddpwdclemdc  12175  ennnfonelemf1  12421  grpidinv2  12933  dvdsrzring  13578  cncnp2m  13816  bj-charfun  14644